From 1e1c98d47c6a32611f37b5d6da1060c5a09f268c Mon Sep 17 00:00:00 2001 From: Francesco Mazzoli Date: Tue, 11 Jun 2013 01:14:23 +0100 Subject: [PATCH] more report --- examples.ka | 9 ++- itt.ka | 34 +++++++++++ thesis.lagda | 161 +++++++++++++++++++++++++++++++++++++++++---------- 3 files changed, 171 insertions(+), 33 deletions(-) diff --git a/examples.ka b/examples.ka index 45e69e4..072ab79 100644 --- a/examples.ka +++ b/examples.ka @@ -1,3 +1,4 @@ +------------------------------------------------------------ -- Naturals data Nat : * => { zero : Nat | suc : Nat -> Nat } @@ -6,13 +7,18 @@ one : Nat => (suc zero) two : Nat => (suc one) three : Nat => (suc two) +------------------------------------------------------------ -- Binary trees + data Tree : [A : *] -> * => { leaf : Tree A | node : Tree A -> A -> Tree A -> Tree A } +------------------------------------------------------------ -- Empty types + data Empty : * => { } +------------------------------------------------------------ -- Ordered lists record Unit : * => tt { } @@ -37,11 +43,12 @@ le' [l1 : Lift] : Lift -> * => ( (\l2 => Lift-Elim l2 (\_ => *) Empty (\_ => Empty) Unit) ) -data OList : [low : Lift] [upp : Lift] -> * => +data OList : [low upp : Lift] -> * => { nil : le' low upp -> OList low upp | cons : [n : Nat] -> OList (lift n) upp -> le' low (lift n) -> OList low upp } +------------------------------------------------------------ -- Dependent products record Prod : [A : *] [B : A -> *] -> * => diff --git a/itt.ka b/itt.ka index e9decf6..3f81a45 100644 --- a/itt.ka +++ b/itt.ka @@ -1,3 +1,6 @@ +------------------------------------------------------------ +-- Core ITT (minus W) + data Empty : * => { } absurd [A : *] [x : Empty] : A => ( @@ -15,3 +18,34 @@ data Bool : * => { true : Bool | false : Bool } -- The if_then_else_ is provided by Bool-Elim +------------------------------------------------------------ +-- Examples → + +data Nat : * => { zero : Nat | suc : Nat -> Nat } + +gt [n : Nat] : Nat -> * => ( + Nat-Elim + n + (\_ => Nat -> *) + (\_ => Empty) + (\n f m => Nat-Elim m (\_ => *) Unit (\m' _ => f m')) +) + +data List : [A : *] -> * => + { nil : List A | cons : A -> List A -> List A } + +length [A : *] [xs : List A] : Nat => ( + List-Elim xs (\_ => Nat) zero (\_ _ n => suc n) +) + +head [A : *] [xs : List A] : gt (length A xs) zero -> A => ( + List-Elim + xs + (\xs => gt (length A xs) zero -> A) + (\p => absurd A p) + (\x _ _ _ => x) +) + +------------------------------------------------------------ +-- Examples × + diff --git a/thesis.lagda b/thesis.lagda index d7a4864..fa18087 100644 --- a/thesis.lagda +++ b/thesis.lagda @@ -59,7 +59,7 @@ \DeclareUnicodeCharacter{9655}{\ensuremath{\rhd}} \renewenvironment{code}% -{\noindent\ignorespaces\advance\leftskip\mathindent\AgdaCodeStyle\pboxed}% +{\noindent\ignorespaces\advance\leftskip\mathindent\AgdaCodeStyle\pboxed\small}% {\endpboxed\par\noindent% \ignorespacesafterend\small} @@ -197,7 +197,7 @@ \newcommand{\myval}[3]{#1 : #2 \mapsto #3} \newcommand{\mypost}[2]{\mysyn{abstract}\ #1 : #2} \newcommand{\myadt}[4]{\mysyn{data}\ #1 #2\ \mysyn{where}\ #3\{ #4 \}} -\newcommand{\myreco}[4]{\mysyn{record}\ #1 #2\ \mysyn{where}\ #3\ \{ #4 \}} +\newcommand{\myreco}[4]{\mysyn{record}\ #1 #2\ \mysyn{where}\ \{ #4 \}} \newcommand{\myelabt}{\vdash} \newcommand{\myelabf}{\rhd} \newcommand{\myelab}[2]{\myctx \myelabt #1 \myelabf #2} @@ -225,6 +225,7 @@ \newcommand{\mydcsep}{\ |\ } \newcommand{\mytree}{\mytyc{Tree}} \newcommand{\myproj}[1]{\myfun{$\pi_{#1}$}} +\newcommand{\mysigma}{\mytyc{$\Sigma$}} %% ----------------------------------------------------------------------------- @@ -233,30 +234,34 @@ \author{Francesco Mazzoli \href{mailto:fm2209@ic.ac.uk}{\nolinkurl{}}} \date{June 2013} + \iffalse + \begin{code} + module thesis where + \end{code} + \fi + \begin{document} -\iffalse -\begin{code} -module thesis where -\end{code} -\fi +\begin{titlepage} + \centering -\maketitle + \maketitle + \thispagestyle{empty} -\begin{minipage}{0.5\textwidth} + \begin{minipage}{0.4\textwidth} \begin{flushleft} \large \emph{Supervisor:}\\ Dr. Steffen \textsc{van Backel} \end{flushleft} \end{minipage} -\begin{minipage}{0.5\textwidth} +\begin{minipage}{0.4\textwidth} \begin{flushright} \large \emph{Co-marker:} \\ Dr. Philippa \textsc{Gardner} \end{flushright} \end{minipage} -\clearpage +\end{titlepage} \begin{abstract} The marriage between programming and logic has been a very fertile one. In @@ -289,7 +294,8 @@ module thesis where in particular Andrea Vezzosi and James Deikun, with whom I entertained countless insightful discussions in the past year. Andrea suggested Observational Type Theory as a topic of study: this thesis would not - exist without him. + exist without him. Before them, Tony Fields introduced me to Haskell, + unknowingly filling most of my free time from that time on. Finally, much of the work stems from the research of Conor McBride, who answered many of my doubts through these months. I also owe him @@ -338,14 +344,14 @@ formally explained by the $\beta$-reduction rule: $ \begin{array}{l} \myapp{(\myabs{\myb{x}}{\mytmm})}{\mytmn} \myred \mysub{\mytmm}{\myb{x}}{\mytmn}\text{, where} \\ - \myind{1} + \myind{2} \begin{array}{l@{\ }c@{\ }l} \mysub{\myb{x}}{\myb{x}}{\mytmn} & = & \mytmn \\ \mysub{\myb{y}}{\myb{x}}{\mytmn} & = & y\text{, with } \myb{x} \neq y \\ \mysub{(\myapp{\mytmt}{\mytmm})}{\myb{x}}{\mytmn} & = & (\myapp{\mysub{\mytmt}{\myb{x}}{\mytmn}}{\mysub{\mytmm}{\myb{x}}{\mytmn}}) \\ \mysub{(\myabs{\myb{x}}{\mytmm})}{\myb{x}}{\mytmn} & = & \myabs{\myb{x}}{\mytmm} \\ \mysub{(\myabs{\myb{y}}{\mytmm})}{\myb{x}}{\mytmn} & = & \myabs{\myb{z}}{\mysub{\mysub{\mytmm}{\myb{y}}{\myb{z}}}{\myb{x}}{\mytmn}}, \\ - \multicolumn{3}{l}{\myind{1} \text{with $\myb{x} \neq \myb{y}$ and $\myb{z}$ not free in $\myapp{\mytmm}{\mytmn}$}} + \multicolumn{3}{l}{\myind{2} \text{with $\myb{x} \neq \myb{y}$ and $\myb{z}$ not free in $\myapp{\mytmm}{\mytmn}$}} \end{array} \end{array} $ @@ -1654,7 +1660,7 @@ to bottom, making sure that no such proof can exist, and providing an \myexi{\myb{x_1}}{\mytya_1}{\mytyb_1} & \myeq & \myexi{\myb{x_2}}{\mytya_2}{\mytya_2} & \myred \\ \multicolumn{4}{l}{ \myind{2} \mytya_1 \myeq \mytyb_1 \myand - \myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{\myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2}} \myimpl \mytyb_1 \myeq \mytyb_2} + \myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{\myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2}} \myimpl \mytyb_1[\myb{x_1}] \myeq \mytyb_2[\myb{x_2}]} } \\ \myfora{\myb{x_1}}{\mytya_1}{\mytyb_1} & \myeq & \myfora{\myb{x_2}}{\mytya_2}{\mytyb_2} & \myred \cdots \\ \myw{\myb{x_1}}{\mytya_1}{\mytyb_1} & \myeq & \myw{\myb{x_2}}{\mytya_2}{\mytyb_2} & \myred \cdots \\ @@ -1718,19 +1724,20 @@ proof that given equal values in the first element, the types of the second elements are equal too ($\myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{\myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2}} \myimpl \mytyb_1 \myeq \mytyb_2}$)\footnote{We are using $\myimpl$ to - indicate a $\forall$ where we discard the first value. Also note that - the $\myb{x_1}$ in the $\mytyb_1$ inside the $\forall$ is re-bound to - the quantification, and similarly for $\myb{x_2}$ and $\mytyb_2$.}. -This also explains the need for heterogeneous equality, since in the -second proof it would be awkward to express the fact that $\myb{A_1}$ is -the same as $\myb{A_2}$. In the respective $\myfun{coe}$ case, since -the types are canonical, we know at this point that the proof of -equality is a pair of the shape described above. Thus, we can -immediately coerce the first element of the pair using the first element -of the proof, and then instantiate the second element with the two first -elements and a proof by coherence of their equality, since we know that -the types are equal. The cases for the other binders are omitted for -brevity, but they follow the same principle. + indicate a $\forall$ where we discard the first value. We write + $\mytyb_1[\myb{x_1}]$ to indicate that the $\myb{x_1}$ in $\mytyb_1$ + is re-bound to the $\myb{x_1}$ quantified by the $\forall$, and + similarly for $\myb{x_2}$ and $\mytyb_2$.}. This also explains the +need for heterogeneous equality, since in the second proof it would be +awkward to express the fact that $\myb{A_1}$ is the same as $\myb{A_2}$. +In the respective $\myfun{coe}$ case, since the types are canonical, we +know at this point that the proof of equality is a pair of the shape +described above. Thus, we can immediately coerce the first element of +the pair using the first element of the proof, and then instantiate the +second element with the two first elements and a proof by coherence of +their equality, since we know that the types are equal. The cases for +the other binders are omitted for brevity, but they follow the same +principle. \subsubsection{$\myfun{coe}$, laziness, and $\myfun{coh}$erence} @@ -1783,7 +1790,7 @@ axioms as abstracted variables. & \multicolumn{11}{@{}l}{ \myind{2} \myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{ \myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2} \myimpl - \myjm{\myapp{\myse{f}_1}{\myb{x_1}}}{\mytyb_1}{\myapp{\myse{f}_2}{\myb{x_2}}}{\mytyb_2} + \myjm{\myapp{\myse{f}_1}{\myb{x_1}}}{\mytyb_1[\myb{x_1}]}{\myapp{\myse{f}_2}{\myb{x_2}}}{\mytyb_2[\myb{x_2}]} }} } \\ (&\mytmt_1 \mynodee \myse{f}_1 & : & \myw{\mytya_1}{\myb{x_1}}{\mytyb_1}&) & \myeq & (&\mytmt_1 \mynodee \myse{f}_1 & : & \myw{\mytya_2}{\myb{x_2}}{\mytyb_2}&) & \myred \cdots \\ @@ -2110,6 +2117,7 @@ checking the type, and updating the context with a new typed variable: } \subsubsection{User defined types} +\label{sec:user-type} \begin{figure}[p] \begin{subfigure}[b]{\textwidth} @@ -2608,7 +2616,6 @@ is to generate reduction rules and coercions. Before defining $\myprop$, we define some basic types inside $\mykant$, as the target for the $\myprop$ decoder: - \begin{framed} \small $ @@ -2618,7 +2625,7 @@ $ \myind{2} \myabs{\myb{A\ \myb{bot}}}{\mytyc{Empty}.\myfun{elim} \myappsp \myb{bot} \myappsp (\myabs{\_}{\myb{A}})} \\ \ \\ - \myreco{\mytyc{Unit}}{}{\mydc{tt}}{ } \\ \ \\ + \myreco{\mytyc{Unit}}{}{}{ } \\ \ \\ \myreco{\mytyc{Prod}}{\myappsp (\myb{A}\ \myb{B} {:} \mytyp)}{ }{\myfun{fst} : \myb{A}, \myfun{snd} : \myb{B} } \end{array} @@ -2678,6 +2685,95 @@ identify the propositional fragment iinternally \cite{Jacobs1994}. \subsubsection{OTT constructs} +Before presenting the direction that $\mykant$\ takes, let's consider +some examples of use-defined data types, and the result we would expect, +given what we already know about OTT, assuming the same propositional +equalities. + +\begin{description} + +\item[Product types] Let's consider first the already mentioned + dependent product, using the alternate name $\mysigma$\footnote{For + extra confusion, `dependent products' are often called `dependent + sums' in the literature, referring to the interpretation that + identifies the first element as a `tag' deciding the type of the + second element, which lets us recover sum types (disjuctions), as we + saw in section \ref{sec:user-type}. Thus, $\mysigma$.} to + avoid confusion with the $\mytyc{Prod}$ in the prelude: {\small\[ + \begin{array}{@{}l} + \myreco{\mysigma}{\myappsp (\myb{A} {:} \mytyp) \myappsp (\myb{B} {:} \myb{A} \myarr \mytyp)}{\\ \myind{2}}{\myfst : \myb{A}, \mysnd : \myapp{\myb{B}}{\myb{fst}}} + \end{array} + \]} Let's start with type-level equality. The result we want is + {\small\[ + \begin{array}{@{}l} + \mysigma \myappsp \mytya_1 \myappsp \mytyb_1 \myeq \mysigma \myappsp \mytya_2 \myappsp \mytyb_2 \myred \\ + \myind{2} \mytya_1 \myeq \mytya_2 \myand \myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{\myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2}} \myimpl \myapp{\mytyb_1}{\myb{x_1}} \myeq \myapp{\mytyb_2}{\myb{x_2}}} + \end{array} + \]} The difference here is that in the original presentation of OTT + the type binders are explicit, while here $\mytyb_1$ and $\mytyb_2$ + functions returning types. We can do this thanks to the type + hierarchy, and this hints at the fact that heterogeneous equality will + have to allow $\mytyp$ `to the right of the colon', and in fact this + provides the solution to simplify the equality above. + + If we take, just like we saw previously in OTT + {\small\[ + \begin{array}{@{}l} + \myjm{\myse{f}_1}{\myfora{\mytya_1}{\myb{x_1}}{\mytyb_1}}{\myse{f}_2}{\myfora{\mytya_2}{\myb{x_2}}{\mytyb_2}} \myred \\ + \myind{2} \myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{ + \myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2} \myimpl + \myjm{\myapp{\myse{f}_1}{\myb{x_1}}}{\mytyb_1[\myb{x_1}]}{\myapp{\myse{f}_2}{\myb{x_2}}}{\mytyb_2[\myb{x_2}]} + }} + \end{array} + \]} Then we can simply take + {\small\[ + \begin{array}{@{}l} + \mysigma \myappsp \mytya_1 \myappsp \mytyb_1 \myeq \mysigma \myappsp \mytya_2 \myappsp \mytyb_2 \myred \\ \myind{2} \mytya_1 \myeq \mytya_2 \myand \myjm{\mytyb_1}{\mytya_1 \myarr \mytyp}{\mytyb_2}{\mytya_2 \myarr \mytyp} + \end{array} + \]} Which will reduce to precisely what we desire. For what + concerns coercions and quotation, things stay the same (apart from the + fact that we apply to the second argument instead of substituting). + We can recognise records such as $\mysigma$ as such and employ + projections in value equality, coercions, and quotation; as to not + impede progress if not necessary. + +\item[Lists] Now for finite lists, which will give us a taste for data + constructors: + {\small\[ + \begin{array}{@{}l} + \myadt{\mylist}{\myappsp (\myb{A} {:} \mytyp)}{ }{\mydc{nil} \mydcsep \mydc{cons} \myappsp \myb{A} \myappsp (\myapp{\mylist}{\myb{A}})} + \end{array} + \]} + Type equality is simple---we only need to compare the parameter: + {\small\[ + \mylist \myappsp \mytya_1 \myeq \mylist \myappsp \mytya_2 \myred \mytya_1 \myeq \mytya_2 + \]} For coercions, we transport based on the constructor, recycling + the proof for the inductive occurrence: {\small\[ + \begin{array}{@{}l@{\ }c@{\ }l} + \mycoe \myappsp (\mylist \myappsp \mytya_1) \myappsp (\mylist \myappsp \mytya_2) \myappsp \myse{Q} \myappsp \mydc{nil} & \myred & \mydc{nil} \\ + \mycoe \myappsp (\mylist \myappsp \mytya_1) \myappsp (\mylist \myappsp \mytya_2) \myappsp \myse{Q} \myappsp (\mydc{cons} \myappsp \mytmm \myappsp \mytmn) & \myred & \\ + \multicolumn{3}{l}{\myind{2} \mydc{cons} \myappsp (\mycoe \myappsp \mytya_1 \myappsp \mytya_2 \myappsp \myse{Q} \myappsp \mytmm) \myappsp (\mycoe \myappsp (\mylist \myappsp \mytya_1) \myappsp (\mylist \myappsp \mytya_2) \myappsp \myse{Q} \myappsp \mytmn)} + \end{array} + \]} Value equality is unsurprising---we match the constructors, and + return bottom for mismatches. However, we also need to equate the + parameter in $\mydc{nil}$: {\small\[ + \begin{array}{r@{ }c@{\ }c@{\ }c@{}l@{\ }c@{\ }r@{}c@{\ }c@{\ }c@{}l@{\ }l} + (& \mydc{nil} & : & \myapp{\mylist}{\mytya_1} &) & \myeq & (& \mydc{nil} & : & \myapp{\mylist}{\mytya_2} &) \myred \mytya_1 \myeq \mytya_2 \\ + (& \mydc{cons} \myappsp \mytmm_1 \myappsp \mytmn_1 & : & \myapp{\mylist}{\mytya_1} &) & \myeq & (& \mydc{cons} \myappsp \mytmm_2 \myappsp \mytmn_2 & : & \myapp{\mylist}{\mytya_2} &) \myred \\ + & \multicolumn{11}{@{}l}{ \myind{2} + \myjm{\mytmm_1}{\mytya_1}{\mytmm_2}{\mytya_2} \myand \myjm{\mytmn_1}{\myapp{\mylist}{\mytya_1}}{\mytmn_2}{\myapp{\mylist}{\mytya_2}} + } \\ + (& \mydc{nil} & : & \myapp{\mylist}{\mytya_1} &) & \myeq & (& \mydc{cons} \myappsp \mytmm_2 \myappsp \mytmn_2 & : & \myapp{\mylist}{\mytya_2} &) \myred \mybot \\ + (& \mydc{cons} \myappsp \mytmm_1 \myappsp \mytmn_1 & : & \myapp{\mylist}{\mytya_1} &) & \myeq & (& \mydc{nil} & : & \myapp{\mylist}{\mytya_2} &) \myred \mybot + \end{array} + \]} + Finally, quotation + % TODO quotation + + +\end{description} + + \mydesc{syntax}{ }{ $ \begin{array}{r@{\ }c@{\ }l} @@ -2755,7 +2851,8 @@ identify the propositional fragment iinternally \cite{Jacobs1994}. \subsubsection{$\myprop$ and the hierarchy} -Where is $\myprop$ placed in the $\mytyp$ hierarchy? +Where is $\myprop$ placed in the $\mytyp$ hierarchy? At each universe +level, we will have that \subsubsection{Quotation and irrelevance} \ref{sec:kant-irr} -- 2.30.2