idris-proposal.tex

   1 \documentclass[article, a4paper]{article}
   2 \usepackage[T1]{fontenc}
   3 \usepackage{lmodern}
   4 \usepackage{amssymb,amsmath}
   5 \usepackage{bussproofs}
   6
   7 % Provides \textsubscript
   8 \usepackage{fixltx2e}
   9
  10 \usepackage[osf]{libertine}
  11
  12 %\usepackage[T1]{fontenc}
  13 \usepackage{helvet}
  14
  15 % Use microtype if available
  16 \IfFileExists{microtype.sty}{\usepackage{microtype}}{}
  17
  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.
  21 \makeatletter
  22 \def\maxwidth{
  23   \ifdim\Gin@nat@width>\linewidth\linewidth
  24   \else\Gin@nat@width\fi
  25 }
  26 \makeatother
  27
  28 \usepackage[
  29   setpagesize=false, % page size defined by xetex
  30   unicode=false, % unicode breaks when used with xetex
  31   xetex
  32 ]{hyperref}
  33
  34 \hypersetup{
  35   breaklinks=true,
  36   bookmarks=true,
  37   pdfauthor={Francesco Mazzoli <fm2209@ic.ac.uk>},
  38   pdftitle={Scalor + Observational Equality},
  39   colorlinks=false,
  40   pdfborder={0 0 0}
  41 }
  42
  43 % Make links footnotes instead of hotlinks:
  44 \renewcommand{\href}[2]{#2\footnote{\url{#1}}}
  45
  46 \usepackage[normalem]{ulem}
  47 % avoid problems with \sout in headers with hyperref:
  48 \pdfstringdefDisableCommands{\renewcommand{\sout}{}}
  49
  50 \setcounter{secnumdepth}{0}
  51
  52 \title{Scalor + Observational Equality}
  53 \author{Francesco Mazzoli \texttt{\textless{}fm2209@ic.ac.uk\textgreater{}}}
  54 \date{November 2012}
  55
  56 \begin{document}
  57
  58 \maketitle
  59
  60 \section{Type theories and equality}
  61
  62 Scalor is a newly developed dependently typed programming language based on
  63 Idris \cite{Idris},
  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.
  69
  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'':
  73
  74 \begin{prooftree}
  75     \AxiomC{$\Gamma \vdash x : A$}
  76     \AxiomC{$A \equiv B$}
  77     \BinaryInfC{$\Gamma \vdash x : B$}
  78 \end{prooftree}
  79
  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
  82 alpha-renaming.
  83
  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:
  88
  89 \begin{prooftree}
  90     \AxiomC{$\Gamma \vdash x : A$}
  91     \UnaryInfC{$\Gamma \vdash \mathsf{refl}_A\ x : x =_A x$}
  92 \end{prooftree}
  93
  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:
  97
  98 \begin{prooftree}
  99     \AxiomC{$\Gamma \vdash p : x =_A y$}
 100     \UnaryInfC{$\Gamma \vdash x \equiv y : A$}
 101 \end{prooftree}
 102
 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.
 106
 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.
 111
 112 However, this expressive power comes at a price: type checking is
 113 undecidable, and the system fails to be strongly normalising.
 114
 115 \section{Observational equality}
 116
 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
 123 value unchanged.
 124
 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:
 128
 129 \begin{itemize}
 130 \item
 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.
 137 \item
 138   Implement the above, and adjust the elaboration of the high level
 139   language to work with the extended \texttt{TT}.
 140 \item
 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.
 145 \end{itemize}
 146
 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.
 150
 151 \begin{thebibliography}{1}
 152
 153 \bibitem{OTT}
 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.
 157
 158 \bibitem{Idris}
 159   Edwin McBrady. Idris. \url{http://www.idris-lang.org}.
 160
 161 \bibitem{Epigram}
 162   Conor McBride et al. Epigram, 2004. \url{http://e-pig.org}.
 163
 164 \bibitem{Agda}
 165   Ulf Norell. Agda 2. \url{http://wiki.portal.chalmers.se/agda/pmwiki.php}.
 166
 167 \bibitem{Coq}
 168   INRIA. Coq. \url{http://coq.inria.fr/}.
 169
 170 \end{thebibliography}
 171
 172 \end{document}