1 files changed, 172 insertions, 0 deletions
diff --git a/idris-proposal.tex b/idris-proposal.tex
new file mode 100644
index 0000000..1d7a043
--- /dev/null
+++ b/idris-proposal.tex
@@ -0,0 +1,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}