1 \documentclass[article, a4paper]{article}
2 \usepackage[T1]{fontenc}
4 \usepackage{amssymb,amsmath}
5 \usepackage{bussproofs}
7 % Provides \textsubscript
10 \usepackage[osf]{libertine}
12 %\usepackage[T1]{fontenc}
15 % Use microtype if available
16 \IfFileExists{microtype.sty}{\usepackage{microtype}}{}
18 % We will generate all images so they have a width \maxwidth. This means
19 % that they will get their normal width if they fit onto the page, but
20 % are scaled down if they would overflow the margins.
23 \ifdim\Gin@nat@width>\linewidth\linewidth
24 \else\Gin@nat@width\fi
29 setpagesize=false, % page size defined by xetex
30 unicode=false, % unicode breaks when used with xetex
37 pdfauthor={Francesco Mazzoli <fm2209@ic.ac.uk>},
38 pdftitle={Scalor + Observational Equality},
43 % Make links footnotes instead of hotlinks:
44 \renewcommand{\href}[2]{#2\footnote{\url{#1}}}
46 \usepackage[normalem]{ulem}
47 % avoid problems with \sout in headers with hyperref:
48 \pdfstringdefDisableCommands{\renewcommand{\sout}{}}
50 \setcounter{secnumdepth}{0}
52 \title{Scalor + Observational Equality}
53 \author{Francesco Mazzoli \texttt{\textless{}fm2209@ic.ac.uk\textgreater{}}}
60 \section{Type theories and equality}
62 Scalor is a newly developed dependently typed programming language based on
64 \href{https://en.wikipedia.org/wiki/Intuitionistic\_type\_theory}{Intuitionistic
65 Type Theory} (ITT), in the tradition of Agda \cite{Agda}, Epigram
66 \cite{Epigram}, and Coq \cite{Coq}. Contrary to these languages, Idris puts the
67 focus on programming rather than on theorem proving, with the goal of bringing
68 dependent types to the programming practice.
70 Type theories of this family will need a notion of \emph{definitional}
71 equality ($\equiv$), used by the type checker to determine if two terms
72 are convertible and thus treatable as ``the same thing'':
75 \AxiomC{$\Gamma \vdash x : A$}
77 \BinaryInfC{$\Gamma \vdash x : B$}
80 In Idris and in the languages cited above, this amounts to reduce the
81 terms to their unique normal form and then compare them up to
84 However, it is also useful to have a notion of equality \emph{inside}
85 the type theory, as a type, to enable the user to reason about equality
86 in proofs. This takes the name of \emph{propositional} equality, and is
87 reasonably introduced by reflexivity:
90 \AxiomC{$\Gamma \vdash x : A$}
91 \UnaryInfC{$\Gamma \vdash \mathsf{refl}_A\ x : x =_A x$}
94 Some type theories include a rule that allows definitional equality to
95 be derived from propositional equality, thus allowing types to impact
96 significantly on the type-checking procedure:
99 \AxiomC{$\Gamma \vdash p : x =_A y$}
100 \UnaryInfC{$\Gamma \vdash x \equiv y : A$}
103 Systems that have this property are known as \emph{extensional}, as
104 opposed to \emph{intensional} systems that lack it. Idris and all the
105 languages cited fall in the latter category.
107 Extensional type theories (ETTs) allow more terms to be typed. For
108 example, many higher-order properties such as
109 \[\mathsf{map}\ (f \circ g) = \mathsf{map}\ f \circ \mathsf{map}\ g\]
110 can only be proved in extensional type theories.
112 However, this expressive power comes at a price: type checking is
113 undecidable, and the system fails to be strongly normalising.
115 \section{Observational equality}
117 To solve this issues Altenkirch, McBride, and Swiestra introduced
118 ``Observational Type Theory'' \cite{OTT} (OTT). In this context, the
119 user can manually transport (``coerce'') values between types given
120 appropriate proofs of equality. The trick is to compute the equality
121 between types and values by inspecting them (the ``observation''), at
122 the same time guaranteeing that each coercion will effectively leave the
125 This system allows the expressive power given by ETT, while maintaining
126 the good properties of ITT. We propose to extend Idris to include the
127 facilities provided by OTT. A rough outline of the path to get there is:
131 Figure out how to extend the Idris' core type theory, ``\texttt{TT}'',
132 to support coercions. The main missing piece is the universe
133 hierarchy, although Conor McBride provided an
134 \href{http://www.e-pig.org/epilogue/?p=1098}{Agda embedding} of OTT
135 for a hierarchy of universes. OTT also uses W-types to represent
136 inductive families, while \texttt{TT} uses families directly.
138 Implement the above, and adjust the elaboration of the high level
139 language to work with the extended \texttt{TT}.
141 Implement high level facilities to include coercions. This would
142 consist of setting up syntax for the user to use and figuring out how
143 to elaborate it to \texttt{TT}, possibly with some inference to
144 include coercions automatically, at least in some cases.
147 Considering the novelty of the theory and the practical approach of the
148 language, we are excited at the possibilities and new developments that
149 this addition would bring.
151 \begin{thebibliography}{1}
154 T. Altenkirch, C. McBride, and W. Swierstra. Observational equality, now! In
155 \emph{Proceedings of the 2007 workshop on Programming languages meets program
156 verification}, PLPV ’07, pages 57–68, New York, NY, USA, 2007. ACM.
159 Edwin McBrady. Idris. \url{http://www.idris-lang.org}.
162 Conor McBride et al. Epigram, 2004. \url{http://e-pig.org}.
165 Ulf Norell. Agda 2. \url{http://wiki.portal.chalmers.se/agda/pmwiki.php}.
168 INRIA. Coq. \url{http://coq.inria.fr/}.
170 \end{thebibliography}