From b1c43d9ab075249fd141e99ce4934dbd1ea67fc8 Mon Sep 17 00:00:00 2001 From: Francesco Mazzoli Date: Fri, 14 Dec 2012 14:29:58 +0000 Subject: [PATCH] initial files --- docs/Makefile | 15 ++++ docs/background.tex | 84 ++++++++++++++++++++ docs/idris-proposal.tex | 172 ++++++++++++++++++++++++++++++++++++++++ 3 files changed, 271 insertions(+) create mode 100644 docs/Makefile create mode 100644 docs/background.tex create mode 100644 docs/idris-proposal.tex diff --git a/docs/Makefile b/docs/Makefile new file mode 100644 index 0000000..cbd2436 --- /dev/null +++ b/docs/Makefile @@ -0,0 +1,15 @@ +SOURCES = $(wildcard *.tex) +OBJECTS = $(patsubst %.tex, %.pdf, $(SOURCES)) + +all: $(OBJECTS) + +%.pdf : %.tex + xelatex -halt-on-error $< + xelatex -halt-on-error $< + +clean: cleanup + rm -f $(OBJECTS) + +cleanup: + rm -f *.log *.aux *.nav *.snm *.toc *.vrb *.out + diff --git a/docs/background.tex b/docs/background.tex new file mode 100644 index 0000000..6e93919 --- /dev/null +++ b/docs/background.tex @@ -0,0 +1,84 @@ +\documentclass[article, a4paper]{article} +\usepackage[T1]{fontenc} +\usepackage{fixltx2e} +\usepackage{enumitem} +\usepackage[normalem]{ulem} +\usepackage{graphicx} +\usepackage{subcaption} + +%% ----------------------------------------------------------------------------- +%% Fonts +%% \usepackage[osf]{libertine} +%% \usepackage{helvet} +%% \usepackage{lmodern} +%% \IfFileExists{microtype.sty}{\usepackage{microtype}}{} + +%% ----------------------------------------------------------------------------- +%% TikZ stuff +%% \usepackage{tikz} +%% \usetikzlibrary{positioning} +%% \usetikzlibrary{shapes} +%% \usetikzlibrary{arrows} +%% \usepackage{tikz-cd} +%% \usepackage{pgfplots} + +%% ----------------------------------------------------------------------------- +%% Symbols +\usepackage{amssymb,amsmath} +\usepackage{wasysym} +\usepackage{turnstile} +\usepackage{centernot} + +%% ----------------------------------------------------------------------------- +%% Utils +\usepackage{bussproofs} +\usepackage{umoline} +\usepackage[export]{adjustbox} +\usepackage{multicol} + +%% Numbering depth +%% \setcounter{secnumdepth}{0} + +%% ----------------------------------------------------------------------------- +% 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 + +%% ----------------------------------------------------------------------------- +%% Links +\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 }, + pdftitle={The Path Towards Observational Equality}, + colorlinks=false, + pdfborder={0 0 0} +} + +% Make links footnotes instead of hotlinks: +\renewcommand{\href}[2]{#2\footnote{\url{#1}}} + +% avoid problems with \sout in headers with hyperref: +\pdfstringdefDisableCommands{\renewcommand{\sout}{}} + +\title{The Path Towards Observational Equality} +\author{Francesco Mazzoli \url{}} +\date{December 2012} + +\begin{document} + +\maketitle + +\end{document} diff --git a/docs/idris-proposal.tex b/docs/idris-proposal.tex new file mode 100644 index 0000000..1d7a043 --- /dev/null +++ b/docs/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 }, + 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} -- 2.30.2