\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}
\newcommand{\myprsyn}{\myse{prop}}
\newcommand{\myprdec}[1]{\mathopen{\mytyc{$\llbracket$}} #1 \mathopen{\mytyc{$\rrbracket$}}}
\newcommand{\myand}{\mathrel{\mytyc{$\wedge$}}}
+\newcommand{\mybigand}{\mathrel{\mytyc{$\bigwedge$}}}
\newcommand{\myprfora}[3]{\forall #1 {:} #2. #3}
\newcommand{\myimpl}{\mathrel{\mytyc{$\Rightarrow$}}}
\newcommand{\mybot}{\mytyc{$\bot$}}
\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}
\newcommand{\mydcsep}{\ |\ }
\newcommand{\mytree}{\mytyc{Tree}}
\newcommand{\myproj}[1]{\myfun{$\pi_{#1}$}}
+\newcommand{\mysigma}{\mytyc{$\Sigma$}}
%% -----------------------------------------------------------------------------
\author{Francesco Mazzoli \href{mailto:fm2209@ic.ac.uk}{\nolinkurl{<fm2209@ic.ac.uk>}}}
\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
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
$
\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}
$
\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 \\
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}
& \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 \\
}
\subsubsection{User defined types}
-
-\begin{figure}[p]
- \begin{subfigure}[b]{\textwidth}
- \vspace{-1cm}
- \mydesc{syntax}{ }{
- \footnotesize
- $
- \begin{array}{l}
- \mynamesyn ::= \cdots \mysynsep \mytyc{D} \mysynsep \mytyc{D}.\mydc{c} \mysynsep \mytyc{D}.\myfun{f}
- \end{array}
- $
- }
-
- \mydesc{syntax elaboration:}{\mydeclsyn \myelabf \mytmsyn ::= \cdots}{
- \footnotesize
- $
- \begin{array}{r@{\ }l}
- & \myadt{\mytyc{D}}{\mytele}{}{\cdots\ |\ \mydc{c}_n : \mytele_n } \\
- \myelabf &
-
- \begin{array}{r@{\ }c@{\ }l}
- \mytmsyn & ::= & \cdots \mysynsep \myapp{\mytyc{D}}{\mytmsyn^{\mytele}} \mysynsep \cdots \mysynsep
- \mytyc{D}.\mydc{c}_n \myappsp \mytmsyn^{\mytele_n} \mysynsep \mytyc{D}.\myfun{elim} \myappsp \mytmsyn \\
- \end{array}
- \end{array}
- $
- }
-
- \mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{
- \footnotesize
-
- \AxiomC{$
- \begin{array}{c}
- \myinf{\mytele \myarr \mytyp}{\mytyp}\hspace{0.8cm}
- \mytyc{D} \not\in \myctx \\
- \myinff{\myctx;\ \mytyc{D} : \mytele \myarr \mytyp}{\mytele \mycc \mytele_i \myarr \myapp{\mytyc{D}}{\mytelee}}{\mytyp}\ \ \ (1 \leq i \leq n) \\
- \text{For each $(\myb{x} {:} \mytya)$ in each $\mytele_i$, if $\mytyc{D} \in \mytya$, then $\mytya = \myapp{\mytyc{D}}{\vec{\mytmt}}$.}
- \end{array}
- $}
- \UnaryInfC{$
- \begin{array}{r@{\ }c@{\ }l}
- \myctx & \myelabt & \myadt{\mytyc{D}}{\mytele}{}{ \cdots \ |\ \mydc{c}_n : \mytele_n } \\
- & & \vspace{-0.2cm} \\
- & \myelabf & \myctx;\ \mytyc{D} : \mytele \myarr \mytyp;\ \cdots;\ \mytyc{D}.\mydc{c}_n : \mytele \mycc \mytele_n \myarr \myapp{\mytyc{D}}{\mytelee}; \\
- & &
- \begin{array}{@{}r@{\ }l l}
- \mytyc{D}.\myfun{elim} : & \mytele \myarr (\myb{x} {:} \myapp{\mytyc{D}}{\mytelee}) \myarr & \textbf{target} \\
- & (\myb{P} {:} \myapp{\mytyc{D}}{\mytelee} \myarr \mytyp) \myarr & \textbf{motive} \\
- & \left.
- \begin{array}{@{}l}
- \myind{3} \vdots \\
- (\mytele_n \mycc \myhyps(\myb{P}, \mytele_n) \myarr \myapp{\myb{P}}{(\myapp{\mytyc{D}.\mydc{c}_n}{\mytelee_n})}) \myarr
- \end{array} \right \}
- & \textbf{methods} \\
- & \myapp{\myb{P}}{\myb{x}} &
- \end{array}
- \end{array}
- $}
- \DisplayProof \\ \vspace{0.2cm}\ \\
- $
- \begin{array}{@{}l l@{\ } l@{} r c l}
- \textbf{where} & \myhyps(\myb{P}, & \myemptytele &) & \mymetagoes & \myemptytele \\
- & \myhyps(\myb{P}, & (\myb{r} {:} \myapp{\mytyc{D}}{\vec{\mytmt}}) \mycc \mytele &) & \mymetagoes & (\myb{r'} {:} \myapp{\myb{P}}{\myb{r}}) \mycc \myhyps(\myb{P}, \mytele) \\
- & \myhyps(\myb{P}, & (\myb{x} {:} \mytya) \mycc \mytele & ) & \mymetagoes & \myhyps(\myb{P}, \mytele)
- \end{array}
- $
-
- }
-
- \mydesc{reduction elaboration:}{\mydeclsyn \myelabf \myctx \vdash \mytmsyn \myred \mytmsyn}{
- \footnotesize
- $\myadt{\mytyc{D}}{\mytele}{}{ \cdots \ |\ \mydc{c}_n : \mytele_n } \ \ \myelabf$
- \AxiomC{$\mytyc{D} : \mytele \myarr \mytyp \in \myctx$}
- \AxiomC{$\mytyc{D}.\mydc{c}_i : \mytele;\mytele_i \myarr \myapp{\mytyc{D}}{\mytelee} \in \myctx$}
- \BinaryInfC{$
- \myctx \vdash \myapp{\myapp{\myapp{\mytyc{D}.\myfun{elim}}{(\myapp{\mytyc{D}.\mydc{c}_i}{\vec{\myse{t}}})}}{\myse{P}}}{\vec{\myse{m}}} \myred \myapp{\myapp{\myse{m}_i}{\vec{\mytmt}}}{\myrecs(\myse{P}, \vec{m}, \mytele_i)}
- $}
- \DisplayProof \\ \vspace{0.2cm}\ \\
- $
- \begin{array}{@{}l l@{\ } l@{} r c l}
- \textbf{where} & \myrecs(\myse{P}, \vec{m}, & \myemptytele &) & \mymetagoes & \myemptytele \\
- & \myrecs(\myse{P}, \vec{m}, & (\myb{r} {:} \myapp{\mytyc{D}}{\vec{A}}); \mytele & ) & \mymetagoes & (\mytyc{D}.\myfun{elim} \myappsp \myb{r} \myappsp \myse{P} \myappsp \vec{m}); \myrecs(\myse{P}, \vec{m}, \mytele) \\
- & \myrecs(\myse{P}, \vec{m}, & (\myb{x} {:} \mytya); \mytele &) & \mymetagoes & \myrecs(\myse{P}, \vec{m}, \mytele)
- \end{array}
- $
- }
- \end{subfigure}
-
- \begin{subfigure}[b]{\textwidth}
- \mydesc{syntax elaboration:}{\myelab{\mydeclsyn}{\mytmsyn ::= \cdots}}{
- \footnotesize
- $
- \begin{array}{r@{\ }c@{\ }l}
- \myctx & \myelabt & \myreco{\mytyc{D}}{\mytele}{}{ \cdots, \myfun{f}_n : \myse{F}_n } \\
- & \myelabf &
-
- \begin{array}{r@{\ }c@{\ }l}
- \mytmsyn & ::= & \cdots \mysynsep \myapp{\mytyc{D}}{\mytmsyn^{\mytele}} \mysynsep \mytyc{D}.\mydc{constr} \myappsp \mytmsyn^{n} \mysynsep \cdots \mysynsep \mytyc{D}.\myfun{f}_n \myappsp \mytmsyn \\
- \end{array}
- \end{array}
- $
-}
-
-
-\mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{
- \footnotesize
- \AxiomC{$
- \begin{array}{c}
- \myinf{\mytele \myarr \mytyp}{\mytyp}\hspace{0.8cm}
- \mytyc{D} \not\in \myctx \\
- \myinff{\myctx; \mytele; (\myb{f}_j : \myse{F}_j)_{j=1}^{i - 1}}{F_i}{\mytyp} \myind{3} (1 \le i \le n)
- \end{array}
- $}
- \UnaryInfC{$
- \begin{array}{r@{\ }c@{\ }l}
- \myctx & \myelabt & \myreco{\mytyc{D}}{\mytele}{}{ \cdots, \myfun{f}_n : \myse{F}_n } \\
- & & \vspace{-0.2cm} \\
- & \myelabf & \myctx;\ \mytyc{D} : \mytele \myarr \mytyp;\ \cdots;\ \mytyc{D}.\myfun{f}_n : \mytele \myarr (\myb{x} {:} \myapp{\mytyc{D}}{\mytelee}) \myarr \mysub{\myse{F}_n}{\myb{f}_i}{\myapp{\myfun{f}_i}{\myb{x}}}_{i = 1}^{n-1}; \\
- & & \mytyc{D}.\mydc{constr} : \mytele \myarr \myse{F}_1 \myarr \cdots \myarr \myse{F}_n \myarr \myapp{\mytyc{D}}{\mytelee};
- \end{array}
- $}
- \DisplayProof
-}
-
- \mydesc{reduction elaboration:}{\mydeclsyn \myelabf \myctx \vdash \mytmsyn \myred \mytmsyn}{
- \footnotesize
- $\myreco{\mytyc{D}}{\mytele}{}{ \cdots, \myfun{f}_n : \myse{F}_n } \ \ \myelabf$
- \AxiomC{$\mytyc{D} \in \myctx$}
- \UnaryInfC{$\myctx \vdash \myapp{\mytyc{D}.\myfun{f}_i}{(\mytyc{D}.\mydc{constr} \myappsp \vec{t})} \myred t_i$}
- \DisplayProof
- }
-
- \end{subfigure}
- \caption{Elaboration for data types and records.}
- \label{fig:elab}
-\end{figure}
+\label{sec:user-type}
Elaborating user defined types is the real effort. First, let's explain
what we can defined, with some examples.
What we have is equivalent to ITT's dependent products.
\end{description}
+\begin{figure}[p]
+ \begin{subfigure}[b]{\textwidth}
+ \vspace{-1cm}
+ \mydesc{syntax}{ }{
+ \footnotesize
+ $
+ \begin{array}{l}
+ \mynamesyn ::= \cdots \mysynsep \mytyc{D} \mysynsep \mytyc{D}.\mydc{c} \mysynsep \mytyc{D}.\myfun{f}
+ \end{array}
+ $
+ }
+
+ \mydesc{syntax elaboration:}{\mydeclsyn \myelabf \mytmsyn ::= \cdots}{
+ \footnotesize
+ $
+ \begin{array}{r@{\ }l}
+ & \myadt{\mytyc{D}}{\mytele}{}{\cdots\ |\ \mydc{c}_n : \mytele_n } \\
+ \myelabf &
+
+ \begin{array}{r@{\ }c@{\ }l}
+ \mytmsyn & ::= & \cdots \mysynsep \myapp{\mytyc{D}}{\mytmsyn^{\mytele}} \mysynsep \cdots \mysynsep
+ \mytyc{D}.\mydc{c}_n \myappsp \mytmsyn^{\mytele_n} \mysynsep \mytyc{D}.\myfun{elim} \myappsp \mytmsyn \\
+ \end{array}
+ \end{array}
+ $
+ }
+
+ \mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{
+ \footnotesize
+
+ \AxiomC{$
+ \begin{array}{c}
+ \myinf{\mytele \myarr \mytyp}{\mytyp}\hspace{0.8cm}
+ \mytyc{D} \not\in \myctx \\
+ \myinff{\myctx;\ \mytyc{D} : \mytele \myarr \mytyp}{\mytele \mycc \mytele_i \myarr \myapp{\mytyc{D}}{\mytelee}}{\mytyp}\ \ \ (1 \leq i \leq n) \\
+ \text{For each $(\myb{x} {:} \mytya)$ in each $\mytele_i$, if $\mytyc{D} \in \mytya$, then $\mytya = \myapp{\mytyc{D}}{\vec{\mytmt}}$.}
+ \end{array}
+ $}
+ \UnaryInfC{$
+ \begin{array}{r@{\ }c@{\ }l}
+ \myctx & \myelabt & \myadt{\mytyc{D}}{\mytele}{}{ \cdots \ |\ \mydc{c}_n : \mytele_n } \\
+ & & \vspace{-0.2cm} \\
+ & \myelabf & \myctx;\ \mytyc{D} : \mytele \myarr \mytyp;\ \cdots;\ \mytyc{D}.\mydc{c}_n : \mytele \mycc \mytele_n \myarr \myapp{\mytyc{D}}{\mytelee}; \\
+ & &
+ \begin{array}{@{}r@{\ }l l}
+ \mytyc{D}.\myfun{elim} : & \mytele \myarr (\myb{x} {:} \myapp{\mytyc{D}}{\mytelee}) \myarr & \textbf{target} \\
+ & (\myb{P} {:} \myapp{\mytyc{D}}{\mytelee} \myarr \mytyp) \myarr & \textbf{motive} \\
+ & \left.
+ \begin{array}{@{}l}
+ \myind{3} \vdots \\
+ (\mytele_n \mycc \myhyps(\myb{P}, \mytele_n) \myarr \myapp{\myb{P}}{(\myapp{\mytyc{D}.\mydc{c}_n}{\mytelee_n})}) \myarr
+ \end{array} \right \}
+ & \textbf{methods} \\
+ & \myapp{\myb{P}}{\myb{x}} &
+ \end{array}
+ \end{array}
+ $}
+ \DisplayProof \\ \vspace{0.2cm}\ \\
+ $
+ \begin{array}{@{}l l@{\ } l@{} r c l}
+ \textbf{where} & \myhyps(\myb{P}, & \myemptytele &) & \mymetagoes & \myemptytele \\
+ & \myhyps(\myb{P}, & (\myb{r} {:} \myapp{\mytyc{D}}{\vec{\mytmt}}) \mycc \mytele &) & \mymetagoes & (\myb{r'} {:} \myapp{\myb{P}}{\myb{r}}) \mycc \myhyps(\myb{P}, \mytele) \\
+ & \myhyps(\myb{P}, & (\myb{x} {:} \mytya) \mycc \mytele & ) & \mymetagoes & \myhyps(\myb{P}, \mytele)
+ \end{array}
+ $
+
+ }
+
+ \mydesc{reduction elaboration:}{\mydeclsyn \myelabf \myctx \vdash \mytmsyn \myred \mytmsyn}{
+ \footnotesize
+ $\myadt{\mytyc{D}}{\mytele}{}{ \cdots \ |\ \mydc{c}_n : \mytele_n } \ \ \myelabf$
+ \AxiomC{$\mytyc{D} : \mytele \myarr \mytyp \in \myctx$}
+ \AxiomC{$\mytyc{D}.\mydc{c}_i : \mytele;\mytele_i \myarr \myapp{\mytyc{D}}{\mytelee} \in \myctx$}
+ \BinaryInfC{$
+ \myctx \vdash \myapp{\myapp{\myapp{\mytyc{D}.\myfun{elim}}{(\myapp{\mytyc{D}.\mydc{c}_i}{\vec{\myse{t}}})}}{\myse{P}}}{\vec{\myse{m}}} \myred \myapp{\myapp{\myse{m}_i}{\vec{\mytmt}}}{\myrecs(\myse{P}, \vec{m}, \mytele_i)}
+ $}
+ \DisplayProof \\ \vspace{0.2cm}\ \\
+ $
+ \begin{array}{@{}l l@{\ } l@{} r c l}
+ \textbf{where} & \myrecs(\myse{P}, \vec{m}, & \myemptytele &) & \mymetagoes & \myemptytele \\
+ & \myrecs(\myse{P}, \vec{m}, & (\myb{r} {:} \myapp{\mytyc{D}}{\vec{A}}); \mytele & ) & \mymetagoes & (\mytyc{D}.\myfun{elim} \myappsp \myb{r} \myappsp \myse{P} \myappsp \vec{m}); \myrecs(\myse{P}, \vec{m}, \mytele) \\
+ & \myrecs(\myse{P}, \vec{m}, & (\myb{x} {:} \mytya); \mytele &) & \mymetagoes & \myrecs(\myse{P}, \vec{m}, \mytele)
+ \end{array}
+ $
+ }
+ \end{subfigure}
+
+ \begin{subfigure}[b]{\textwidth}
+ \mydesc{syntax elaboration:}{\myelab{\mydeclsyn}{\mytmsyn ::= \cdots}}{
+ \footnotesize
+ $
+ \begin{array}{r@{\ }c@{\ }l}
+ \myctx & \myelabt & \myreco{\mytyc{D}}{\mytele}{}{ \cdots, \myfun{f}_n : \myse{F}_n } \\
+ & \myelabf &
+
+ \begin{array}{r@{\ }c@{\ }l}
+ \mytmsyn & ::= & \cdots \mysynsep \myapp{\mytyc{D}}{\mytmsyn^{\mytele}} \mysynsep \mytyc{D}.\mydc{constr} \myappsp \mytmsyn^{n} \mysynsep \cdots \mysynsep \mytyc{D}.\myfun{f}_n \myappsp \mytmsyn \\
+ \end{array}
+ \end{array}
+ $
+}
+
+
+\mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{
+ \footnotesize
+ \AxiomC{$
+ \begin{array}{c}
+ \myinf{\mytele \myarr \mytyp}{\mytyp}\hspace{0.8cm}
+ \mytyc{D} \not\in \myctx \\
+ \myinff{\myctx; \mytele; (\myb{f}_j : \myse{F}_j)_{j=1}^{i - 1}}{F_i}{\mytyp} \myind{3} (1 \le i \le n)
+ \end{array}
+ $}
+ \UnaryInfC{$
+ \begin{array}{r@{\ }c@{\ }l}
+ \myctx & \myelabt & \myreco{\mytyc{D}}{\mytele}{}{ \cdots, \myfun{f}_n : \myse{F}_n } \\
+ & & \vspace{-0.2cm} \\
+ & \myelabf & \myctx;\ \mytyc{D} : \mytele \myarr \mytyp;\ \cdots;\ \mytyc{D}.\myfun{f}_n : \mytele \myarr (\myb{x} {:} \myapp{\mytyc{D}}{\mytelee}) \myarr \mysub{\myse{F}_n}{\myb{f}_i}{\myapp{\myfun{f}_i}{\myb{x}}}_{i = 1}^{n-1}; \\
+ & & \mytyc{D}.\mydc{constr} : \mytele \myarr \myse{F}_1 \myarr \cdots \myarr \myse{F}_n \myarr \myapp{\mytyc{D}}{\mytelee};
+ \end{array}
+ $}
+ \DisplayProof
+}
+
+ \mydesc{reduction elaboration:}{\mydeclsyn \myelabf \myctx \vdash \mytmsyn \myred \mytmsyn}{
+ \footnotesize
+ $\myreco{\mytyc{D}}{\mytele}{}{ \cdots, \myfun{f}_n : \myse{F}_n } \ \ \myelabf$
+ \AxiomC{$\mytyc{D} \in \myctx$}
+ \UnaryInfC{$\myctx \vdash \myapp{\mytyc{D}.\myfun{f}_i}{(\mytyc{D}.\mydc{constr} \myappsp \vec{t})} \myred t_i$}
+ \DisplayProof
+ }
+
+ \end{subfigure}
+ \caption{Elaboration for data types and records.}
+ \label{fig:elab}
+\end{figure}
+
Following the intuition given by the examples, the mechanised
elaboration is presented in figure \ref{fig:elab}, which is essentially
a modification of figure 9 of \citep{McBride2004}\footnote{However, our
\DisplayProof
}
-\subsubsection{Why user defined types?}
+\subsubsection{Why user defined types? Why eliminators?}
% TODO reference levitated theories, indexed containers
Before defining $\myprop$, we define some basic types inside $\mykant$,
as the target for the $\myprop$ decoder:
-
\begin{framed}
\small
$
\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}
It is worth to ask if $\myprop$ is needed at all. It is perfectly
possible to have the type checker identify propositional types
automatically, and in fact that is what The author initially planned to
-identify the propositional fragment iinternally \cite{Jacobs1994}.
+identify the propositional fragment internally \cite{Jacobs1994}.
+
+% TODO finish
\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}
$
}
+\begin{figure}[p]
+\mydesc{typing:}{\myctx \vdash \myprsyn \myred \myprsyn}{
+ \footnotesize
+ \begin{tabular}{cc}
+ \AxiomC{$\myjud{\myse{P}}{\myprdec{\mytya \myeq \mytyb}}$}
+ \AxiomC{$\myjud{\mytmt}{\mytya}$}
+ \BinaryInfC{$\myjud{\mycoee{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\mytyb}$}
+ \DisplayProof
+ &
+ \AxiomC{$\myjud{\myse{P}}{\myprdec{\mytya \myeq \mytyb}}$}
+ \AxiomC{$\myjud{\mytmt}{\mytya}$}
+ \BinaryInfC{$\myjud{\mycohh{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\myprdec{\myjm{\mytmt}{\mytya}{\mycoee{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\mytyb}}}$}
+ \DisplayProof
+ \end{tabular}
+}
+\mydesc{propositions:}{\myjud{\myprsyn}{\myprop}}{
+ \footnotesize
+ \begin{tabular}{cc}
+ \AxiomC{\phantom{$\myjud{\myse{P}}{\myprop}$}}
+ \UnaryInfC{$\myjud{\mytop}{\myprop}$}
+ \noLine
+ \UnaryInfC{$\myjud{\mybot}{\myprop}$}
+ \DisplayProof
+ &
+ \AxiomC{$\myjud{\myse{P}}{\myprop}$}
+ \AxiomC{$\myjud{\myse{Q}}{\myprop}$}
+ \BinaryInfC{$\myjud{\myse{P} \myand \myse{Q}}{\myprop}$}
+ \noLine
+ \UnaryInfC{\phantom{$\myjud{\mybot}{\myprop}$}}
+ \DisplayProof
+ \end{tabular}
+
+ \myderivsp
+
+ \begin{tabular}{cc}
+ \AxiomC{$
+ \begin{array}{@{}c}
+ \phantom{\myjud{\myse{A}}{\mytyp} \hspace{0.8cm} \myjud{\mytmm}{\myse{A}}} \\
+ \myjud{\myse{A}}{\mytyp}\hspace{0.8cm}
+ \myjudd{\myctx; \myb{x} : \mytya}{\myse{P}}{\myprop}
+ \end{array}
+ $}
+ \UnaryInfC{$\myjud{\myprfora{\myb{x}}{\mytya}{\myse{P}}}{\myprop}$}
+ \DisplayProof
+ &
+ \AxiomC{$
+ \begin{array}{c}
+ \myjud{\myse{A}}{\mytyp} \hspace{0.8cm} \myjud{\mytmm}{\myse{A}} \\
+ \myjud{\myse{B}}{\mytyp} \hspace{0.8cm} \myjud{\mytmn}{\myse{B}}
+ \end{array}
+ $}
+ \UnaryInfC{$\myjud{\myjm{\mytmm}{\myse{A}}{\mytmn}{\myse{B}}}{\myprop}$}
+ \DisplayProof
+ \end{tabular}
+}
+ % TODO equality for decodings
\mydesc{equality reduction:}{\myctx \vdash \myprsyn \myred \myprsyn}{
\footnotesize
+ \AxiomC{}
+ \UnaryInfC{$\myctx \vdash \myjm{\mytyp}{\mytyp}{\mytyp}{\mytyp} \myred \mytop$}
+ \DisplayProof
+
+ \myderivsp
+
\AxiomC{}
\UnaryInfC{$
- \begin{array}{r@{\ }l}
+ \begin{array}{@{}r@{\ }l}
\myctx \vdash &
\myjm{\myfora{\myb{x_1}}{\mytya_1}{\mytyb_1}}{\mytyp}{\myfora{\myb{x_2}}{\mytya_2}{\mytyb_2}}{\mytyp} \myred \\
- & \myind{2} \mytya_2 \myeq \mytya_1 \myand \\
- & \myind{2} \myprfora{\myb{x_2}}{\mytya_2}{\myprfora{\myb{x_1}}{\mytya_1}{
+ & \myind{2} \mytya_2 \myeq \mytya_1 \myand \myprfora{\myb{x_2}}{\mytya_2}{\myprfora{\myb{x_1}}{\mytya_1}{
\myjm{\myb{x_2}}{\mytya_2}{\myb{x_1}}{\mytya_1} \myimpl \mytyb_1 \myeq \mytyb_2
}}
\end{array}
\myderivsp
- \AxiomC{$\mytyc{D} : \mytele \myarr \mytyp \in \myctx$}
+ \AxiomC{}
\UnaryInfC{$
- \begin{array}{r@{\ }l}
+ \begin{array}{@{}r@{\ }l}
\myctx \vdash &
- \myjm{\mytyc{D} \myappsp \vec{A}}{\mytyp}{\mytyc{D} \myappsp \vec{B}}{\mytyp} \myred \\
- & \myind{2} \myjm{\mytya_1}{\myhead(\mytele)}{\mytyb_1}{\myhead(\mytele)} \myand \cdots \myand \\
- & \myind{2} \myjm{\mytya_n}{\myhead(\mytele(A_1 \cdots A_{n-1}))}{\mytyb_n}{\myhead(\mytele(B_1 \cdots B_{n-1}))}
+ \myjm{\myse{f}_1}{\myfora{\myb{x_1}}{\mytya_1}{\mytyb_1}}{\myse{f}_2}{\myfora{\myb{x_2}}{\mytya_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}
$}
\DisplayProof
+
\myderivsp
- \AxiomC{}
- \UnaryInfC{$\myctx \vdash \myjm{\mytyp}{\mytyp}{\mytyp}{\mytyp} \myred \mytop$}
+ \AxiomC{$\mytyc{D} : \mytele \myarr \mytyp \in \myctx$}
+ \UnaryInfC{$
+ \begin{array}{r@{\ }l}
+ \myctx \vdash &
+ \myjm{\mytyc{D} \myappsp \vec{A}}{\mytyp}{\mytyc{D} \myappsp \vec{B}}{\mytyp} \myred \\
+ & \myind{2} \mybigand_{i = 1}^n (\myjm{\mytya_n}{\myhead(\mytele(A_1 \cdots A_{i-1}))}{\mytyb_i}{\myhead(\mytele(B_1 \cdots B_{i-1}))})
+ \end{array}
+ $}
\DisplayProof
\myderivsp
\AxiomC{$
- \begin{array}{c}
+ \begin{array}{@{}c}
\mydataty(\mytyc{D}, \myctx)\hspace{0.8cm}
- \mytyc{D}.\mydc{c}_i : \mytele;\mytele' \myarr \mytyc{D} \myappsp \mytelee \in \myctx \\
+ \mytyc{D}.\mydc{c} : \mytele;\mytele' \myarr \mytyc{D} \myappsp \mytelee \in \myctx \\
\mytele_A = (\mytele;\mytele')\vec{A}\hspace{0.8cm}
\mytele_B = (\mytele;\mytele')\vec{B}
\end{array}
$}
\UnaryInfC{$
- \begin{array}{l}
- \myctx \vdash \myjm{\mytyc{D}.\mydc{c}_i \myappsp \vec{\mytmm}}{\mytyc{D} \myappsp \vec{A}}{\mytyc{D}.\mydc{c}_i \myappsp \vec{\mytmn}}{\mytyc{D} \myappsp \vec{B}} \myred \\
- \myind{2} \myjm{\mytmm_1}{\myhead(\mytele_A)}{\mytmn_1}{\myhead(\mytele_B)} \myand \cdots \myand \\
- \myind{2} \myjm{\mytmm_n}{\mytya_n}{\mytmn_n}{\mytyb_n}
+ \begin{array}{@{}l@{\ }l}
+ \myctx \vdash & \myjm{\mytyc{D}.\mydc{c} \myappsp \vec{\myse{l}}}{\mytyc{D} \myappsp \vec{A}}{\mytyc{D}.\mydc{c} \myappsp \vec{\myse{r}}}{\mytyc{D} \myappsp \vec{B}} \myred \\
+ & \myind{2} \mybigand_{i=1}^n(\myjm{\mytmm_i}{\myhead(\mytele_A (\mytya_i \cdots \mytya_{i-1}))}{\mytmn_i}{\myhead(\mytele_B (\mytyb_i \cdots \mytyb_{i-1}))})
\end{array}
$}
\DisplayProof
\myderivsp
- \AxiomC{$\myisreco(\mytyc{D}, \myctx)$}
- \UnaryInfC{$\myctx \vdash \myjm{\mytmm}{\mytyc{D} \myappsp \vec{A}}{\mytmn}{\mytyc{D} \myappsp \vec{B}} \myred foo$}
+ \AxiomC{$\mydataty(\mytyc{D}, \myctx)$}
+ \UnaryInfC{$
+ \myctx \vdash \myjm{\mytyc{D}.\mydc{c} \myappsp \vec{\myse{l}}}{\mytyc{D} \myappsp \vec{A}}{\mytyc{D}.\mydc{c'} \myappsp \vec{\myse{r}}}{\mytyc{D} \myappsp \vec{B}} \myred \mybot
+ $}
+ \DisplayProof
+
+ \myderivsp
+
+ \AxiomC{$
+ \begin{array}{@{}c}
+ \myisreco(\mytyc{D}, \myctx)\hspace{0.8cm}
+ \mytyc{D}.\myfun{f}_i : \mytele; (\myb{x} {:} \myapp{\mytyc{D}}{\mytelee}) \myarr \myse{F}_i \in \myctx\\
+ \end{array}
+ $}
+ \UnaryInfC{$
+ \begin{array}{@{}l@{\ }l}
+ \myctx \vdash & \myjm{\myse{l}}{\mytyc{D} \myappsp \vec{A}}{\myse{r}}{\mytyc{D} \myappsp \vec{B}} \myred \\ & \myind{2} \mybigand_{i=1}^n(\myjm{\mytyc{D}.\myfun{f}_1 \myappsp \myse{l}}{(\mytele; (\myb{x} {:} \myapp{\mytyc{D}}{\mytelee}) \myarr \myse{F}_i)(\vec{\mytya};\myse{l})}{\mytyc{D}.\myfun{f}_i \myappsp \myse{r}}{(\mytele; (\myb{x} {:} \myapp{\mytyc{D}}{\mytelee}) \myarr \myse{F}_i)(\vec{\mytyb};\myse{r})})
+ \end{array}
+ $}
\DisplayProof
\myderivsp
\AxiomC{}
- \UnaryInfC{$\mytya \myeq \mytyb \myred \mybot\ \text{if $\mytya$ and $\mytyb$ are canonical types.}$}
+ \UnaryInfC{$\myjm{\mytmm}{\mytya}{\mytmn}{\mytyb} \myred \mybot\ \text{if $\mytya$ and $\mytyb$ are canonical types.}$}
\DisplayProof
}
+ \caption{Equality reduction for $\mykant$.}
+ \label{fig:kant-eq-red}
+\end{figure}
\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}
\label{fig:kant-process}
\end{figure}
-\subsection{Parsing and Sugar}
+\subsection{Parsing and \texttt{Sugar}}
\subsection{Term representation and context}
\label{sec:term-repr}
projects / bitonic-mengthesis.git / blobdiff