From cd099f2777c907e5d8353878627de123c877dc5a Mon Sep 17 00:00:00 2001 From: Francesco Mazzoli Date: Wed, 9 Jan 2013 15:54:05 +0000 Subject: [PATCH] report report --- docs/Makefile | 3 +- docs/background.tex | 276 +++++++++++++++++++++++++++----------------- 2 files changed, 169 insertions(+), 110 deletions(-) diff --git a/docs/Makefile b/docs/Makefile index 33b552c..b22e99b 100644 --- a/docs/Makefile +++ b/docs/Makefile @@ -17,5 +17,4 @@ clean: cleanup rm -f $(OBJECTS) cleanup: - rm -f *.log *.aux *.nav *.snm *.toc *.vrb *.out *.bbl - + rm -f *.log *.aux *.nav *.snm *.toc *.vrb *.out *.bbl *.blg diff --git a/docs/background.tex b/docs/background.tex index ff7595a..ac451f8 100644 --- a/docs/background.tex +++ b/docs/background.tex @@ -111,7 +111,7 @@ programming and theorem proving. Along with Turing's machines, the earliest attempts to formalise computation lead to the $\lambda$-calculus \citep{Church1936}. This early programming -language encodes computation with a minimal sintax and most notably no ``data'' +language encodes computation with a minimal sintax and most notably no `data' in the traditional sense, but just functions. The syntax of $\lambda$-terms consists of just three things: variables, @@ -130,6 +130,7 @@ abstractions, and applications: \newcommand{\termsyn}{\mathit{term}} \newcommand{\axname}[1]{\textbf{#1}} \newcommand{\axdesc}[2]{\axname{#1} \fbox{$#2$}} +\newcommand{\lcsyn}[1]{\mathrm{\underline{#1}}} \begin{center} \axname{syntax} @@ -149,18 +150,19 @@ to avoid problems with name capturing. Intuitively, abstractions applications ($\app{\termt}{\termm}$) apply a function ($\termt$) to an argument ($\termm$). -The ``applying'' is more formally explained with a reduction rule: +The `applying' is more formally explained with a reduction rule: \newcommand{\bred}{\leadsto} \newcommand{\bredc}{\bred^*} \begin{center} \axdesc{reduction}{\termsyn \bred \termsyn} -$$\app{(\abs{x}{\termt})}{\termm} \bred \termt[\termm / x]$$ +$$\app{(\abs{x}{\termt})}{\termm} \bred \termt[\termm ]$$ \end{center} -Where $\termt[\termm / x]$ expresses the operation that substitutes all -occurrences of $x$ with $\termm$ in $\termt$. In the systems presented, the +Where $\termt[\termm ]$ expresses the operation that substitutes all +occurrences of $x$ with $\termm$ in $\termt$. In the future, I will use +$[\termt]$ as an abbreviation for $[\termt ]$. In the systems presented, the $\bred$ relation also includes reduction of subterms, for example if $\termt \bred \termm$ then $\app{\termt}{\termn} \bred \app{\termm}{\termn}$, and so on. @@ -168,12 +170,12 @@ $\bred$ relation also includes reduction of subterms, for example if $\termt These few elements are of remarkable expressiveness, and in fact Turing complete. As a corollary, we must be able to devise a term that reduces forever -(``loops'' in imperative terms): +(`loops' in imperative terms): \begin{equation*} - \app{(\abs{x}{\app{x}{x}})}{(\abs{x}{\app{x}{x}})} \bred \app{(\abs{x}{\app{x}{x}})}{(\abs{x}{\app{x}{x}})} \bred \dots + \app{(\abs{x}{\app{x}{x}})}{(\abs{x}{\app{x}{x}})} \bred \app{(\abs{x}{\app{x}{x}})}{(\abs{x}{\app{x}{x}})} \bred \dotsb \end{equation*} Terms that can be reduced only a finite number of times (the non-looping ones) -are said to be \emph{normalising}, and the ``final'' term is called \emph{normal +are said to be \emph{normalising}, and the `final' term is called \emph{normal form}. These concepts (reduction and normal forms) will run through all the material analysed. @@ -183,12 +185,12 @@ material analysed. \newcommand{\tyb}{B} \newcommand{\tyc}{C} -One way to ``discipline'' $\lambda$-terms is to assign \emph{types} to them, and +One way to `discipline' $\lambda$-terms is to assign \emph{types} to them, and then check that the terms that we are forming make sense given our typing rules \citep{Curry1934}. We wish to introduce rules of the form $\Gamma \vdash \termt : \tya$, which -reads ``in context $\Gamma$, term $\termt$ has type $\tya$''. +reads `in context $\Gamma$, term $\termt$ has type $\tya$'. The syntax for types is as follows: @@ -205,7 +207,7 @@ The syntax for types is as follows: I will use $\tya,\tyb,\dots$ to indicate a generic type. A context $\Gamma$ is a map from variables to types. We use the notation -$\Gamma; x : \tya$ to augment it, and to ``extract'' pairs from it. +$\Gamma; x : \tya$ to augment it, and to `extract' pairs from it. Predictably, $\tya \tyarr \tyb$ is the type of a function from $\tya$ to $\tyb$. We need to be able to decorate our abstractions with @@ -242,12 +244,12 @@ Now we are ready to give the typing judgements: \end{tabular} \end{center} -This typing system takes the name of ``simply typed lambda calculus'' (STLC), +This typing system takes the name of `simply typed lambda calculus' (STLC), and enjoys a number of properties. Two of them are expected in most type systems: %TODO add credit to pierce \begin{description} \item[Progress] A well-typed term is not stuck - either it is a value or it can - take a step according to the evaluation rules. With ``value'' we mean a term + take a step according to the evaluation rules. With `value' we mean a term whose subterms (including itself) don't appear to the left of the $\bred$ relation. \item[Preservation] If a well-typed term takes a step of evaluation, then the @@ -275,7 +277,7 @@ adding a combinator that recurses: \end{prooftree} \end{center} \begin{equation*} - \lcfix{x : \tya}{\termt} \bred \termt[(\lcfix{x : \tya}{\termt}) / x] + \lcfix{x : \tya}{\termt} \bred \termt[(\lcfix{x : \tya}{\termt}) ] \end{equation*} However, we will keep STLC without such a facility. In the next section we shall @@ -284,14 +286,14 @@ see why that is preferable for our needs. \subsection{The Curry-Howard correspondence} \label{sec:curry-howard} -\newcommand{\lcunit}{\mathsf{()}} +\newcommand{\lcunit}{\mathsf{\langle\rangle}} It turns out that the STLC can be seen a natural deduction system for propositional logic. Terms are proofs, and their types are the propositions they prove. This remarkable fact is known as the Curry-Howard correspondence, or isomorphism. -The ``arrow'' ($\to$) type corresponds to implication. If we wished to +The `arrow' ($\to$) type corresponds to implication. If we wished to prove that $(\tya \tyarr \tyb) \tyarr (\tyb \tyarr \tyc) \tyarr (\tya \tyarr \tyc)$, all we need to do is to devise a $\lambda$-term that has the correct type: @@ -308,7 +310,7 @@ Conversely, $\top$ is the type with just one trivial element, $\lcunit$. \newcommand{\lcinl}{\mathsf{inl}\appspace} \newcommand{\lcinr}{\mathsf{inr}\appspace} -\newcommand{\lccase}[3]{\mathsf{case}\appspace#1\appspace#2\appspace#3} +\newcommand{\lccase}[3]{\lcsyn{case}\appspace#1\appspace\lcsyn{of}\appspace#2\appspace#3} \newcommand{\lcfst}{\mathsf{fst}\appspace} \newcommand{\lcsnd}{\mathsf{snd}\appspace} \newcommand{\orint}{\vee I_{1,2}} @@ -319,6 +321,7 @@ Conversely, $\top$ is the type with just one trivial element, $\lcunit$. \newcommand{\andel}{\wedge E_{1,2}} \newcommand{\botel}{\bot E} \newcommand{\lcabsurd}{\mathsf{absurd}\appspace} +\newcommand{\lcabsurdd}[1]{\mathsf{absurd}_{#1}\appspace} \begin{center} \axname{syntax} @@ -367,7 +370,7 @@ Conversely, $\top$ is the type with just one trivial element, $\lcunit$. \begin{tabular}{c c} \AxiomC{$\Gamma \vdash \termt : \bot$} \RightLabel{$\botel$} - \UnaryInfC{$\Gamma \vdash \lcabsurd \termt : \tya$} + \UnaryInfC{$\Gamma \vdash \lcabsurdd{\tya} \termt : \tya$} \DisplayProof & \AxiomC{} @@ -409,7 +412,7 @@ unsound\footnote{Obviously such a term can be present under a $\lambda$.}. \subsection{Extending the STLC} \newcommand{\lctype}{\mathsf{Type}} -\newcommand{\lcite}[3]{\mathsf{if}\appspace#1\appspace\mathsf{then}\appspace#2\appspace\mathsf{else}\appspace#3} +\newcommand{\lcite}[3]{\lcsyn{if}\appspace#1\appspace\lcsyn{then}\appspace#2\appspace\lcsyn{else}\appspace#3} \newcommand{\lcbool}{\mathsf{Bool}} \newcommand{\lcforallz}[2]{\forall #1 \absspace.\absspace #2} \newcommand{\lcforall}[3]{\forall #1 : #2 \absspace.\absspace #3} @@ -444,14 +447,14 @@ Here $\lambda{\to}$, in the bottom left, is the STLC. From there can move along are based on this discipline. \item[Types depending on types (towards $\lambda{\underline{\omega}}$)] In other words, we have type operators: $(\abs{A : \lctype}{\abs{R : \lctype}{(A \to R) \to R}}) : \lctype \to \lctype \to \lctype$. -\item[Types depending on terms (towards $\lambda{P}$)] Also known as ``dependent - types'', give great expressive power: $(\abs{x : \lcbool}{\lcite{x}{\mathbb{N}}{\mathbb{Q}}}) : \lcbool \to \lctype$. +\item[Types depending on terms (towards $\lambda{P}$)] Also known as `dependent + types', give great expressive power: $(\abs{x : \lcbool}{\lcite{x}{\mathbb{N}}{\mathbb{Q}}}) : \lcbool \to \lctype$. \end{description} All the systems preserve the properties that make the STLC well behaved (some of which I haven't mentioned yet). The system we are going to focus on, Intuitionistic Type Theory, has all of the above additions, and thus would sit -where $\lambda{C}$ sits in the ``$\lambda$-cube'' above. +where $\lambda{C}$ sits in the `$\lambda$-cube' above. \section{Intuitionistic Type Theory} @@ -470,10 +473,10 @@ reason he gave a revised and consistent definition later \citep{Martin-Lof1984}. A related development is the one of the polymorphic $\lambda$-calculus, and specifically the previously mentioned System F, which was invented independently -by Girard and Reynolds. An can be found in \citep{Reynolds1994}. The +by Girard and Reynolds. An overview can be found in \citep{Reynolds1994}. The surprising fact is that while System F is impredicative it is still consistent -and strongly normalising. Coquand and Huet further extended this line of work -with the Calculus of Constructions (CoC) \citep{Coquand1986}. +and strongly normalising. \cite{Coquand1986} Huet further extended this line of +work with the Calculus of Constructions (CoC). \subsection{A Core Type Theory} \label{sec:core-tt} @@ -487,8 +490,8 @@ found in \citep{Martin-Lof1984}. \begin{eqnarray*} \termsyn & ::= & x \\ & | & \lcforall{x}{\termsyn}{\termsyn} \separ \abs{x : \termsyn}{\termsyn} \separ \app{\termsyn}{\termsyn} \\ - & | & \lcexists{x}{\termsyn}{\termsyn} \separ (\termsyn , \termsyn) \separ \lcfst \termsyn \separ \lcsnd \termsyn \\ - & | & \bot \separ \lcabsurd \termt \\ + & | & \lcexists{x}{\termsyn}{\termsyn} \separ (\termsyn , \termsyn)_{x.\termsyn} \separ \lcfst \termsyn \separ \lcsnd \termsyn \\ + & | & \bot \separ \lcabsurd_{\termsyn} \termsyn \\ & | & \lcset{n} \\ n & \in & \mathbb{N} \end{eqnarray*} @@ -504,13 +507,11 @@ found in \citep{Martin-Lof1984}. \DisplayProof & \AxiomC{$\Gamma \vdash \termt : \bot$} - \RightLabel{$\bot E$} - \UnaryInfC{$\Gamma \vdash \lcabsurd \termt : A$} + \UnaryInfC{$\Gamma \vdash \lcabsurdd{\tya} \termt : \tya$} \DisplayProof & \AxiomC{$\Gamma \vdash \termt : \tya$} \AxiomC{$\tya \defeq \tyb$} - \RightLabel{$\defeq$ type} \BinaryInfC{$\Gamma \vdash \termt : \tyb$} \DisplayProof \end{tabular} @@ -519,14 +520,12 @@ found in \citep{Martin-Lof1984}. \begin{tabular}{c c} \AxiomC{$\Gamma;x : \tya \vdash \termt : \tya$} - \RightLabel{$\forall I$} \UnaryInfC{$\Gamma \vdash \abs{x : \tya}{\termt} : \lcforall{x}{\tya}{\tyb}$} \DisplayProof & \AxiomC{$\Gamma \vdash \termt : \lcforall{x}{\tya}{\tyb}$} \AxiomC{$\Gamma \vdash \termm : \tya$} - \RightLabel{$\forall E$} - \BinaryInfC{$\Gamma \vdash \app{\termt}{\termm} : \tyb[\termm / x]$} + \BinaryInfC{$\Gamma \vdash \app{\termt}{\termm} : \tyb[\termm ]$} \DisplayProof \end{tabular} @@ -534,16 +533,14 @@ found in \citep{Martin-Lof1984}. \begin{tabular}{c c} \AxiomC{$\Gamma \vdash \termt : \tya$} - \AxiomC{$\Gamma \vdash \termm : \tyb[\termt / x]$} - \RightLabel{$\exists I$} - \BinaryInfC{$\Gamma \vdash (\termt, \termm) : \lcexists{x}{\tya}{\tyb}$} + \AxiomC{$\Gamma \vdash \termm : \tyb[\termt ]$} + \BinaryInfC{$\Gamma \vdash (\termt, \termm)_{x.\tyb} : \lcexists{x}{\tya}{\tyb}$} \DisplayProof & \AxiomC{$\Gamma \vdash \termt: \lcexists{x}{\tya}{\tyb}$} - \RightLabel{$\exists E_{1,2}$} \UnaryInfC{$\hspace{0.7cm} \Gamma \vdash \lcfst \termt : \tya \hspace{0.7cm}$} \noLine - \UnaryInfC{$\Gamma \vdash \lcsnd \termt : \tyb[\lcfst \termt / x]$} + \UnaryInfC{$\Gamma \vdash \lcsnd \termt : \tyb[\lcfst \termt ]$} \DisplayProof \end{tabular} @@ -551,13 +548,11 @@ found in \citep{Martin-Lof1984}. \begin{tabular}{c c} \AxiomC{} - \RightLabel{type} \UnaryInfC{$\Gamma \vdash \lcset{n} : \lcset{n + 1}$} \DisplayProof & \AxiomC{$\Gamma \vdash \tya : \lcset{n}$} \AxiomC{$\Gamma; x : \tya \vdash \tyb : \lcset{m}$} - \RightLabel{$\forall, \exists$ type} \BinaryInfC{$\Gamma \vdash \lcforall{x}{\tya}{\tyb} : \lcset{n \sqcup m}$} \noLine \UnaryInfC{$\Gamma \vdash \lcexists{x}{\tya}{\tyb} : \lcset{n \sqcup m}$} @@ -568,48 +563,46 @@ found in \citep{Martin-Lof1984}. \axdesc{reduction}{\termsyn \bred \termsyn} \begin{eqnarray*} - \app{(\abs{x}{\termt})}{\termm} & \bred & \termt[\termm / x] \\ + \app{(\abs{x}{\termt})}{\termm} & \bred & \termt[\termm ] \\ \lcfst (\termt, \termm) & \bred & \termt \\ \lcsnd (\termt, \termm) & \bred & \termm \end{eqnarray*} \end{center} -I will abbreviate $\lcset{0}$ as $\lcsetz$. - There are a lot of new factors at play here. The first thing to notice is that the separation between types and terms is gone. All we have is terms, that include both values (terms of type $\lcset{0}$) and types (terms of type $\lcset{n}$, with $n > 0$). This change is reflected in the typing rules. While in the STLC values and types are kept well separated (values never go -``right of the colon''), in ITT types can freely depend on values. +`right of the colon'), in ITT types can freely depend on values. This relation is expressed in the typing rules for $\forall$ and $\exists$: if a function has type $\lcforall{x}{\tya}{\tyb}$, $\tyb$ can depend on $x$. -Examples will make this clearer once some base types are added in the next -section. +Examples will make this clearer once some base types are added in section +\ref{sec:base-types}. $\forall$ and $\exists$ are at the core of the machinery of ITT: \begin{description} -\item[``forall'' ($\forall$)] is a generalisation of $\tyarr$ in the STLC and +\item[`forall' ($\forall$)] is a generalisation of $\tyarr$ in the STLC and expresses universal quantification in our logic. In the literature this is - also known as ``dependent product'' and shown as $\Pi$, following the + also known as `dependent product' and shown as $\Pi$, following the interpretation of functions as infinitary products. We will just call it - ``dependent function'', reserving ``product'' for $\exists$. + `dependent function', reserving `product' for $\exists$. -\item[``exists'' ($\exists$)] is a generalisation of $\wedge$ in the extended - STLC of section \ref{sec:curry-howard}, and thus we will call it ``dependent - product''. Like $\wedge$, it is formed by providing a pair of things. In our +\item[`exists' ($\exists$)] is a generalisation of $\wedge$ in the extended + STLC of section \ref{sec:curry-howard}, and thus we will call it `dependent + product'. Like $\wedge$, it is formed by providing a pair of things. In our logic, it represents existential quantification. For added confusion, in the literature that calls $\forall$ $\Pi$, $\exists$ - is often named ``dependent sum'' and shown as $\Sigma$. This is following the + is often named `dependent sum' and shown as $\Sigma$. This is following the interpretation of $\exists$ as a generalised, infinitary $\vee$, where the - first element of the pair is the ``tag'' that decides which type the second + first element of the pair is the `tag' that decides which type the second element will have. \end{description} -Another thing to notice is that types are very ``first class'': we are free to +Another thing to notice is that types are very `first class': we are free to create functions that accept and return types. For this reason we $\defeq$ as the smallest equivalence relation extending $\bredc$, where $\bredc$ is the reflexive transitive closure of $\bred$; and we treat types that are equal @@ -626,9 +619,9 @@ $\app{(\abs{x : \lctype}{x})}{\lcbool} \defeq \lcbool$. The theme of equality is central and will be analysed better later. The theory presented is \emph{stratified}. We have a hierarchy of types -$\lcset{0} : \lcset{1} : \lcset{2} : \dots$, so that there is no ``type of all -types'', and our theory is predicative. The layers of the hierarchy are called -``universes''. $\lcsetz : \lcsetz$ ITT is inconsistent due to Girard's paradox +$\lcset{0} : \lcset{1} : \lcset{2} : \dots$, so that there is no `type of all +types', and our theory is predicative. The layers of the hierarchy are called +`universes'. $\lcsetz : \lcsetz$ ITT is inconsistent due to Girard's paradox \citep{Hurkens1995}, and thus loses its well-behavedness. Some impredicativity sometimes has its place, either because the theory retain good properties (normalization, consistency, etc.) anyway, like in System F and CoC; or because @@ -642,29 +635,50 @@ Lastly, the theory I present is fully explicit in the sense that the user has to specify every type when forming abstractions, products, etc. This can be a great burden if one wants to use the theory directly. Complete inference is undecidable (which is hardly surprising considering the role that types play) -but partial inference (also called ``bidirectional type checking'' in this +but partial inference (also called `bidirectional type checking' in this context) in the style of \citep{Pierce2000} will have to be deployed in a -practical system. When showing examples obvious types will be omitted. +practical system. When showing examples obvious types will be omitted when this +can be done without loss of clarity. Note that the Curry-Howard correspondence runs through ITT as it did with the STLC with the difference that ITT corresponds to an higher order propositional logic. +% TODO describe abbreviations somewhere +% I will use various abbreviations: +% \begin{itemize} +% \item $\lcsetz$ for $\lcset{0}$ +% \item $\tya \tyarr \tyb$ for $\lcforall{-}{\tya}{\tyb}$, when $\tyb$ does not +% depend on the value of type $\tya$ +% \item $( + \subsection{Base Types} +\label{sec:base-types} + +\newcommand{\lctrue}{\mathsf{true}} +\newcommand{\lcfalse}{\mathsf{false}} +\newcommand{\lcw}[3]{\mathsf{W} #1 : #2 \absspace.\absspace #3} +\newcommand{\lcnode}[4]{#1 \lhd_{#2 . #3} #4} +\newcommand{\lcnodez}[2]{#1 \lhd #2} +\newcommand{\lcited}[5]{\lcsyn{if}\appspace#1/#2\appspace.\appspace#3\appspace\lcsyn{then}\appspace#4\appspace\lcsyn{else}\appspace#5} +\newcommand{\lcrec}[4]{\lcsyn{rec}\appspace#1/#2\appspace.\appspace#3\appspace\lcsyn{with}\appspace#4} +\newcommand{\lcrecz}[2]{\lcsyn{rec}\appspace#1\appspace\lcsyn{with}\appspace#2} +\newcommand{\AxiomL}[1]{\Axiom$\fCenter #1$} +\newcommand{\UnaryInfL}[1]{\UnaryInf$\fCenter #1$} While the ITT presented is a fairly complete logic, it is not that useful for programming. If we wish to make it better, we can add some base types to represent the data structures we know and love, such as numbers, lists, and -trees. - -\newcommand{\lctrue}{\mathsf{true}} -\newcommand{\lcfalse}{\mathsf{false}} +trees. Apart from some unsurprising data types, we introduce $\mathsf{W}$, a +very general tree-like structure useful to represent inductively defined types. \begin{center} \axname{syntax} \begin{eqnarray*} \termsyn & ::= & ... \\ - & | & \lcbool \separ \lctrue \separ \lcfalse + & | & \top \separ \lcunit \\ + & | & \lcbool \separ \lctrue \separ \lcfalse \separ \lcited{\termsyn}{x}{\termsyn}{\termsyn}{\termsyn} \\ + & | & \lcw{x}{\termsyn}{\termsyn} \separ \lcnode{\termsyn}{x}{\termsyn}{\termsyn} \separ \lcrec{\termsyn}{x}{\termsyn}{\termsyn} \end{eqnarray*} \axdesc{typing}{\Gamma \vdash \termsyn : \termsyn} @@ -673,68 +687,58 @@ trees. \begin{tabular}{c c c} \AxiomC{} - \RightLabel{var} - \UnaryInfC{$\Gamma;x : \tya \vdash x : \tya$} + \UnaryInfC{$\hspace{0.2cm}\Gamma \vdash \top : \lcset{0} \hspace{0.2cm}$} + \noLine + \UnaryInfC{$\Gamma \vdash \lcbool : \lcset{0}$} \DisplayProof & - \AxiomC{$\Gamma \vdash \termt : \bot$} - \RightLabel{$\bot E$} - \UnaryInfC{$\Gamma \vdash \lcabsurd \termt : A$} + \AxiomC{} + \UnaryInfC{$\Gamma \vdash \lcunit : \top$} \DisplayProof & - \AxiomC{$\Gamma \vdash \termt : \tya$} - \AxiomC{$\tya \defeq \tyb$} - \RightLabel{$\defeq$ type} - \BinaryInfC{$\Gamma \vdash \termt : \tyb$} + \AxiomC{} + \RightLabel{$\lcbool I_{1,2}$} + \UnaryInfC{$\Gamma \vdash \lctrue : \lcbool$} + \noLine + \UnaryInfC{$\Gamma \vdash \lcfalse : \lcbool$} \DisplayProof \end{tabular} \vspace{0.5cm} - \begin{tabular}{c c} - \AxiomC{$\Gamma;x : \tya \vdash \termt : \tya$} - \RightLabel{$\forall I$} - \UnaryInfC{$\Gamma \vdash \abs{x : \tya}{\termt} : \lcforall{x}{\tya}{\tyb}$} + \begin{tabular}{c} + \AxiomC{$\Gamma \vdash \termt : \lcbool$} + \AxiomC{$\Gamma \vdash \termm : \tya[\lctrue]$} + \AxiomC{$\Gamma \vdash \termn : \tya[\lcfalse]$} + \TrinaryInfC{$\Gamma \vdash \lcited{\termt}{x}{\tya}{\termm}{\termn} : \tya[\termt]$} \DisplayProof - & - \AxiomC{$\Gamma \vdash \termt : \lcforall{x}{\tya}{\tyb}$} - \AxiomC{$\Gamma \vdash \termm : \tya$} - \RightLabel{$\forall E$} - \BinaryInfC{$\Gamma \vdash \app{\termt}{\termm} : \tyb[\termm / x]$} + \end{tabular} + + \vspace{0.5cm} + + \begin{tabular}{c} + \AxiomC{$\Gamma \vdash \tya : \lcset{n}$} + \AxiomC{$\Gamma; x : \tya \vdash \tyb : \lcset{m}$} + \BinaryInfC{$\Gamma \vdash \lcw{x}{\tya}{\tyb} : \lcset{n \sqcup m}$} \DisplayProof \end{tabular} \vspace{0.5cm} - \begin{tabular}{c c} + \begin{tabular}{c} \AxiomC{$\Gamma \vdash \termt : \tya$} - \AxiomC{$\Gamma \vdash \termm : \tyb[\termt / x]$} - \RightLabel{$\exists I$} - \BinaryInfC{$\Gamma \vdash (\termt, \termm) : \lcexists{x}{\tya}{\tyb}$} - \DisplayProof - & - \AxiomC{$\Gamma \vdash \termt: \lcexists{x}{\tya}{\tyb}$} - \RightLabel{$\exists E_{1,2}$} - \UnaryInfC{$\hspace{0.7cm} \Gamma \vdash \lcfst \termt : \tya \hspace{0.7cm}$} - \noLine - \UnaryInfC{$\Gamma \vdash \lcsnd \termt : \tyb[\lcfst \termt / x]$} + \AxiomC{$\Gamma \vdash \termf : \tyb[\termt ] \tyarr \lcw{x}{\tya}{\tyb}$} + \BinaryInfC{$\Gamma \vdash \lcnode{\termt}{x}{\tyb}{\termf} : \lcw{x}{\tya}{\tyb}$} \DisplayProof \end{tabular} \vspace{0.5cm} - \begin{tabular}{c c} - \AxiomC{} - \RightLabel{type} - \UnaryInfC{$\Gamma \vdash \lcset{n} : \lcset{n + 1}$} - \DisplayProof - & - \AxiomC{$\Gamma \vdash \tya : \lcset{n}$} - \AxiomC{$\Gamma; x : \tya \vdash \tyb : \lcset{m}$} - \RightLabel{$\forall, \exists$ type} - \BinaryInfC{$\Gamma \vdash \lcforall{x}{\tya}{\tyb} : \lcset{n \sqcup m}$} + \begin{tabular}{c} + \AxiomC{$\Gamma \vdash \termt: \lcw{x}{\tya}{\tyb}$} \noLine - \UnaryInfC{$\Gamma \vdash \lcexists{x}{\tya}{\tyb} : \lcset{n \sqcup m}$} + \UnaryInfC{$\Gamma \vdash \lcforall{\termm}{\tya}{\lcforall{\termf}{(\tyb[\termm] \tyarr \lcw{x}{\tya}{\tyb})}{(\lcforall{\termn}{\tyb[\termm]}{\tyc[\app{\termf}{\termn}]}) \tyarr \tyc[\lcnodez{\termm}{\termf}]}}$} + \UnaryInfC{$\Gamma \vdash \lcrec{\termt}{x}{\tyc}{\termp} : \tyc[\termt]$} \DisplayProof \end{tabular} @@ -742,12 +746,68 @@ trees. \axdesc{reduction}{\termsyn \bred \termsyn} \begin{eqnarray*} - \app{(\abs{x}{\termt})}{\termm} & \bred & \termt[\termm / x] \\ - \lcfst (\termt, \termm) & \bred & \termt \\ - \lcsnd (\termt, \termm) & \bred & \termm + \lcited{\lctrue}{x}{\tya}{\termt}{\termm} & \bred & \termt \\ + \lcited{\lcfalse}{x}{\tya}{\termt}{\termm} & \bred & \termm \\ + \lcrec{\lcnodez{\termt}{\termf}}{x}{\tya}{\termp} & \bred & \app{\app{\app{\termp}{\termt}}{\termf}}{(\abs{\termm}{\lcrec{\app{f}{\termm}}{x}{\tya}{\termp}})} \end{eqnarray*} \end{center} +The introduction and elimination for $\top$ and $\lcbool$ are unsurprising. +Note that in the $\lcite{\dotsb}{\dotsb}{\dotsb}$ construct the type of the +branches are dependent on the value of the conditional. + +The rules for $\mathsf{W}$, on the other hand, are quite an eyesore. The idea +behind $\mathsf{W}$ types is to build up `trees' where shape of the number of +`children' of each node is dependent on the value in the node. This is +captured by the $\lhd$ constructor, where the argument on the left is the value, +and the argument on the right is a function that returns a child for each +possible value of $\tyb[\text{node value}]$, if $\lcw{x}{\tya}{\tyb}$. The +recursor $\lcrec{\termt}{x}{\tyc}{\termp}$ uses $p$ to inductively prove that +$\tyc[\termt]$ holds. + +\subsection{Some examples} + +Now we can finally provide some meaningful examples. I will use some +abbreviations and convenient syntax: +\begin{itemize} + \item $\_\mathit{operator}\_$ to define infix operators + \item $\abs{\{x : \tya\}}{\dotsb}$ to define an abstraction that I will not + explicitly apply since the $x$ can be inferred easily. + \item $\abs{x\appspace y\appspace z : \tya}{\dotsb}$ to define multiple abstractions at the same + time + \item I will omit the explicit typing when forming $\exists$ or $\mathsf{W}$, + and when eliminating $\lcbool$, since the types are almost always clear and + writing them each time is extremely cumbersome. +\end{itemize} + +\subsubsection{Sum types} + +We would like to recover our sum type, or disjunction, $\vee$. This is easily +done with $\exists$: +\begin{eqnarray*} + \_\vee\_ & = & \abs{\tya\appspace\tyb : \lcsetz}{\lcexists{x}{\lcbool}{\lcite{x}{\tya}{\tyb}}} \\ + \lcinl & = & \abs{\{\tya\appspace\tyb : \lcsetz\}}{\abs{x : \tya \vee \tyb}{(\lctrue, x)}} \\ + \lcinr & = & \abs{\{\tya\appspace\tyb : \lcsetz\}}{\abs{x : \tya \vee \tyb}{(\lcfalse, x)}} \\ + \mathsf{case} & = & \abs{\{\tya\appspace\tyb\appspace\tyc : \lcsetz\}}{\abs{x : \tya \vee \tyb}{\abs{f : \tya \tyarr \tyc}{\abs{g : \tyb \tyarr \tyc}{ \\ + & & \hspace{0.5cm} \app{(\lcited{\lcfst x}{b}{(\lcite{b}{A}{B}) \tyarr C}{f}{g})}{(\lcsnd x)}}}}} +\end{eqnarray*} +What is going on here? We are using $\exists$ with $\lcbool$ as a tag, so that +we can choose between one of two types in the second element. In +$\mathsf{case}$ we use $\lcite{\lcfst x}{\dotsb}{\dotsb}$ to discriminate on the +tag, that is, the first element of $x : \tya \vee \tyb$. If the tag is true, +then we know that the second element is of type $\tya$, and we will apply $f$. +The same applies to the other branch, with $\tyb$ and $g$. + +\subsubsection{Naturals and similarly lists} + +Now it's time to showcase the power of $\mathsf{W}$ types. + +\begin{eqnarray*} + \mathsf{Nat} & = & \lcw{b}{\lcbool}{\abs{b}{\lcite{b}{\top}{\bot}}} \\ + \mathsf{zero} & = & \lcfalse \lhd \abs{z}{\lcabsurd z} \\ + \mathsf{suc} & = & \abs{n}{(\lctrue \lhd \abs{\_}{n})} \\ + \mathsf{plus} & = & \abs{x\appspace y}{\lcrecz{x}{\abs{b}{\lcite{b}{\abs{\_\appspace f}{\app{\mathsf{suc}}{(\app{f}{\lcunit})}}}{\abs{\_\appspace\_}{y}}}}} +\end{eqnarray*} \bibliographystyle{authordate1} \bibliography{background} -- 2.30.2