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