\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}