From ebdf439a201d6fda0780284fc7f49b1f8deb88ab Mon Sep 17 00:00:00 2001 From: Francesco Mazzoli Date: Sat, 22 Jun 2013 17:06:40 +0100 Subject: [PATCH] ... --- Makefile | 15 +- thesis.bib => final.bib | 0 thesis.lagda => final.lagda | 223 +++++++------- presentation.tex | 568 ++++++++++++++++++++++++++++++++++++ 4 files changed, 693 insertions(+), 113 deletions(-) rename thesis.bib => final.bib (100%) rename thesis.lagda => final.lagda (97%) create mode 100644 presentation.tex diff --git a/Makefile b/Makefile index d807c24..3fd7f1d 100644 --- a/Makefile +++ b/Makefile @@ -6,16 +6,19 @@ OBJECTS = $(OBJECTST) $(OBJECTSA) all: $(OBJECTS) -thesis.pdf: thesis.tex thesis.bib agda.sty +final.pdf: final.tex final.bib agda.sty pdflatex -halt-on-error $< -o $@ - bibtex thesis + bibtex final pdflatex -halt-on-error $< -o $@ pdflatex -halt-on-error $< -o $@ -agda.sty: thesis.tex +presentation.pdf: presentation.tex + pdflatex -halt-on-error $< -o $@ + +agda.sty: final.tex -thesis.tex: thesis.lagda - agda --allow-unsolved-metas --latex --latex-dir . -i . -i ~/src/agda-lib/src/ thesis.lagda +final.tex: final.lagda + agda --allow-unsolved-metas --latex --latex-dir . -i . -i ~/src/agda-lib/src/ final.lagda InterimReport.pdf: InterimReport.tex InterimReport.bib InterimReport.agda xelatex -halt-on-error $< -o $@ @@ -29,7 +32,7 @@ idris-proposal.pdf: idris-proposal.tex clean: cleanup rm -f $(OBJECTS) - rm -f thesis.tex agda.sty + rm -f final.tex cleanup: rm -f *.log *.aux *.nav *.snm *.toc *.vrb *.out *.bbl *.blg *.agdai diff --git a/thesis.bib b/final.bib similarity index 100% rename from thesis.bib rename to final.bib diff --git a/thesis.lagda b/final.lagda similarity index 97% rename from thesis.lagda rename to final.lagda index 77fdd95..8928ec7 100644 --- a/thesis.lagda +++ b/final.lagda @@ -2,7 +2,7 @@ %% THIS LATEX HURTS YOUR EYES. DO NOT READ. -\documentclass[11pt, fleqn, twoside]{article} +\documentclass[11pt, fleqn, twoside, a4paper]{article} \usepackage{etex} \usepackage[usenames,dvipsnames]{xcolor} @@ -23,7 +23,7 @@ % \headheight 0pt % \headsep 0pt -\usepackage[hmargin=2cm,vmargin=2.5cm]{geometry} +\usepackage[hmargin=2cm,vmargin=2.5cm,a4paper]{geometry} \geometry{textwidth=390pt} \geometry{bindingoffset=1.5cm} @@ -62,6 +62,8 @@ \usepackage{verbatim} \usepackage{fancyvrb} +\usepackage[nottoc]{tocbibind} + \RecustomVerbatimEnvironment {Verbatim}{Verbatim} {xleftmargin=9mm} @@ -316,7 +318,7 @@ hypertexnames=true, pdfhighlight=/O, urlcolor=webbrown, linkcolor=black, citecol \iffalse \begin{code} - module thesis where + module final where \end{code} \fi @@ -378,7 +380,7 @@ hypertexnames=true, pdfhighlight=/O, urlcolor=webbrown, linkcolor=black, citecol To bring OTT closer to the current practice of interactive theorem provers, we describe \mykant, a system featuring OTT in a setting more close to the one found in widely used provers such as Agda and Coq. - Most notably, we feature used defined inductive and record types and a + Most notably, we feature user defined inductive and record types and a cumulative, implicit type hierarchy. Having implemented part of $\mykant$ as a Haskell program, we describe some of the implementation issues faced. @@ -454,7 +456,7 @@ the study of programming languages. In this space, we shall follow the discipline of Intuitionistic Type Theory, or Martin-L\"{o}f Type Theory, after its inventor. First formulated in the 70s and then adjusted through a series of revisions, -it has endured as the core of many practical systems widely in use +it has endured as the core of many practical systems in wide use today, and it is the most prominent instance of the proposition-as-types and proofs-as-programs paradigm. One of the most debated subjects in this field has been regarding what notion of equality should be @@ -496,9 +498,9 @@ and \cite{Martin-Lof1984} himself. Section \ref{sec:equality} will introduce propositional equality. The properties of propositional equality will be discussed along with its -limitations. After reviewing some extensions to propositional equality, -we will explain why identifying definitional equality with propositional -equality causes problems. +limitations. After reviewing some extensions, we will explain why +identifying definitional equality with propositional equality causes +problems. Section \ref{sec:ott} will introduce observational equality, following closely the original exposition by \cite{Altenkirch2007}. The @@ -552,7 +554,7 @@ adopting the proofs-as-programs mantra. The defining features of \mykant\ are: \begin{description} -\item[Full dependent types] In ITT, types are very `first class' notion +\item[Full dependent types] In ITT, types are a very `first class' notion and can be the result of computation---they can \emph{depend} on values, thus the name \emph{dependent types}. \mykant\ espouses this notion to its full consequences. @@ -562,10 +564,10 @@ adopting the proofs-as-programs mantra. The defining features of greater flexibility. We have two kinds of user defined types: inductive data types, formed by various data constructors whose type signatures can contain recursive occurrences of the type being - defined; and records, where we have just one data constructor and + defined; and records, where we have just one data constructor, and projections to extract each each field in said constructor. -\item[Consistency] Our system is meant to be consistent with respects to +\item[Consistency] Our system is meant to be consistent with respect to the logic it embodies. For this reason, we restrict recursion to \emph{structural} recursion on the defined inductive types, through the use of operators (destructors) computing on each type. Following @@ -579,9 +581,9 @@ adopting the proofs-as-programs mantra. The defining features of \cite{Pierce2000}. This cuts down the type annotations by a considerable amount in an elegant way and at a very low cost. Bidirectional type checking is usually employed in core calculi, but - in \mykant\ we extend the concept to user defined data types. + in \mykant\ we extend the concept to user defined types. -\item[Type hierarchy] In set theory we have to take treat powerset-like +\item[Type hierarchy] In set theory we have to take powerset-like objects with care, if we want to avoid paradoxes. However, the working mathematician is rarely concerned by this, and the consistency in this regard is implicitly assumed. In the tradition of @@ -789,7 +791,7 @@ adding a combinator that recurses: \begin{minipage}{0.5\textwidth} \mydesc{syntax}{ } { $ \mytmsyn ::= \cdots b \mysynsep \myfix{\myb{x}}{\mytysyn}{\mytmsyn} $ - \vspace{0.5cm} + \vspace{0.4cm} } \end{minipage} \begin{minipage}{0.5\textwidth} @@ -804,7 +806,7 @@ adding a combinator that recurses: $ \myfix{\myb{x}}{\mytya}{\mytmt} \myred \mysub{\mytmt}{\myb{x}}{(\myfix{\myb{x}}{\mytya}{\mytmt})}$ } -This will deprive us of normalisation, which is a particularly bad thing if we +\mysyn{fix} will deprive us of normalisation, which is a particularly bad thing if we want to use the STLC as described in the next section. Another important property of the STLC is the Church-Rosser property: @@ -1085,12 +1087,12 @@ id :: a -> a id x = x \end{Verbatim} Where \texttt{a} implicitly quantifies over a type, and will be - instantiated automatically thanks to the inference. + instantiated automatically when \texttt{id} is used thanks to the type inference. \item[Types depending on types (towards $\lambda{\underline{\omega}}$)] We have type operators. For example we could define a function that given types $R$ and $\mytya$ forms the type that represents a value of type $\mytya$ in continuation passing style: - \[\displaystyle(\myabss{\myb{R} \myarr \myb{A}}{\mytyp}{(\myb{A} + \[\displaystyle(\myabss{\myb{R} \myappsp \myb{A}}{\mytyp}{(\myb{A} \myarr \myb{R}) \myarr \myb{R}}) : \mytyp \myarr \mytyp \myarr \mytyp \] In Haskell we can define type operator of sorts, although we must @@ -1099,8 +1101,7 @@ id x = x newtype Cont r a = Cont ((a -> r) -> r) \end{Verbatim} Where the `type' (kind in Haskell parlance) of \texttt{Cont} will be - \texttt{* -> * -> *}, with \texttt{*} signifying the type of types in - Haskell. + \texttt{* -> * -> *}, with \texttt{*} signifying the type of types. \item[Types depending on terms (towards $\lambda{P}$)] Also known as `dependent types', give great expressive power. For example, we can have values of whose type depend on a boolean: @@ -1110,12 +1111,12 @@ newtype Cont r a = Cont ((a -> r) -> r) very different language if it did. \end{description} -All the systems preserve the properties that make the STLC well behaved. 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'. It will serve as the logical `core' of all the other -extensions that we will present and ultimately our implementation of a similar -logic. +All the systems placed on the cube preserve the properties that make the +STLC well behaved. The one we are going to focus on, Intuitionistic +Type Theory, has all of the above additions, and thus would sit where +$\lambda{C}$ sits. It will serve as the logical +`core' of all the other extensions that we will present and ultimately +our implementation of a similar logic. \subsection{A Bit of History} @@ -1227,7 +1228,7 @@ The typing rules are presented piece by piece in the following sections. \end{tabular} } -The first thing to notice is that a barrier between values and types that we had +The first thing to notice is that the barrier between values and types that we had in the STLC is gone: values can appear in types, and the two are treated uniformly in the syntax. @@ -1237,8 +1238,8 @@ not immediate as in the STLC. \begin{mydef}[Definitional equality] We define \emph{definitional equality}, $\mydefeq$, as the congruence relation extending -$\myred$. Moreover, when comparing types syntactically we do it up to -renaming of bound names ($\alpha$-renaming) +$\myred$. Moreover, when comparing terms syntactically we do it up to +renaming of bound names ($\alpha$-renaming). \end{mydef} For example under this discipline we will find that \[ @@ -1250,8 +1251,7 @@ For example under this discipline we will find that Types that are definitionally equal can be used interchangeably. Here the `conversion' rule is not syntax directed, but it is possible to employ $\myred$ to decide term equality in a systematic way, comparing -terms by reducing to their normal forms and then comparing them -syntactically; so that a separate conversion rule is not needed. +terms by reducing them to their unique normal forms first; so that a separate conversion rule is not needed. Another thing to notice is that, considering the need to reduce terms to decide equality, for type checking to be decidable a dependently typed must be terminating and confluent; since every type needs to have a @@ -1293,7 +1293,7 @@ see in Section \ref{sec:term-hierarchy}. \end{minipage} \vspace{0.1cm} -We need to refine the notion context to make sure that every variable appearing +We need to refine the notion of context to make sure that every variable appearing is typed correctly, or that in other words each type appearing in the context is indeed a type and not a value. In every other rule, if no premises are present, we assume the context in the conclusion to be valid. @@ -1358,7 +1358,7 @@ sure that we are invoking $\myabsurd{}$ over a type. With booleans we get the first taste of the `dependent' in `dependent types'. While the two introduction rules for $\mytrue$ and $\myfalse$ -are not surprising, the typing rules for $\myfun{if}$ are. In most +are not surprising, the rule for $\myfun{if}$ is. In most strongly typed languages we expect the branches of an $\myfun{if}$ statements to be of the same type, to preserve subject reduction, since execution could take both paths. This is a pity, since the type system @@ -1369,11 +1369,12 @@ if null xs then head xs else 0 \end{Verbatim} are a necessary, well-typed, danger. -However, in a more expressive system, we can do better: the branches' type can -depend on the value of the scrutinised boolean. This is what the typing rule -expresses: the user provides a type $\mytya$ ranging over an $\myb{x}$ -representing the scrutinised boolean type, and the branches are type checked with -the updated knowledge of the value of $\myb{x}$. +However, in a more expressive system, we can do better: the branches' +type can depend on the value of the scrutinised boolean. This is what +the typing rule expresses: the user provides a type $\mytya$ ranging +over an $\myb{x}$ representing the boolean we are operating the +$\myfun{if}$ switch with, and each branch is type checked against +$\mytya$ with the updated knowledge of the value of $\myb{x}$. \subsubsection{$\myarr$, or dependent function} \label{sec:depprod} @@ -1423,12 +1424,13 @@ types \] \myfun{length} is the usual polymorphic length -function. $\myarg\myfun{$>$}\myarg$ is a function that takes two naturals -and returns a type: if the lhs is greater then the rhs, $\myunit$ is -returned, $\myempty$ otherwise. This way, we can express a +function. $\myarg\myfun{$>$}\myarg$ is a function that takes two +naturals and returns a type: if the lhs is greater then the rhs, +$\myunit$ is returned, $\myempty$ otherwise. This way, we can express a `non-emptiness' condition in $\myfun{head}$, by including a proof that the length of the list argument is non-zero. This allows us to rule out -the `empty list' case, so that we can safely return the first element. +the empty list case by invoking \myfun{absurd} in \myfun{length}, so +that we can safely return the first element. Finally, we need to make sure that the type hierarchy is respected, which is the reason why a type formed by $\myarr$ will live in the least upper @@ -1576,7 +1578,7 @@ And with a bit of effort, we can recover addition: they’re no basis for an implementation of recursive data types in decidable type theories.'} For this reasons \mytyc{W}-types have remained nothing more than a reasoning tool, and practical systems - must implement more expressive ways to represent data. + must implement more manageable ways to represent data. \section{The struggle for equality} \label{sec:equality} @@ -1655,7 +1657,8 @@ as the dominating form of equality in systems based on ITT up since Our type former is $\mypeq$, which given a type relates equal terms of that type. $\mypeq$ has one introduction rule, $\myrefl$, which -introduces an equality relation between definitionally equal terms. +introduces an equality between definitionally equal terms---a proof by +reflexivity. Finally, we have one eliminator for $\mypeq$ , $\myjeqq$ (also known as `\myfun{J} axiom' in the literature). @@ -1696,6 +1699,7 @@ regarding equality, such as symmetry, transitivity, congruence laws, etc.\footnote{For definitions of these functions, refer to Appendix \ref{app:itt-code}.} \subsection{Common extensions} +\label{sec:extensions} Our definitional and propositional equalities can be enhanced in various ways. Obviously if we extend the definitional equality we are also @@ -1781,11 +1785,11 @@ Thus, $\myfun{K}$ is derivable in the systems that implement dependent pattern matching, such as Epigram and Agda; but for example not in Coq. $\myfun{K}$ is controversial mainly because it is at odds with -equalities that include computational behaviour, most notably -Voevodsky's \emph{Univalent Foundations}, which feature a \emph{univalence} -axiom that identifies isomorphisms between types with propositional -equality. For example we would have two isomorphisms, and thus two -equalities, between $\mybool$ and $\mybool$, corresponding to the two +equalities that include computational content, most notably Voevodsky's +\emph{Univalent Foundations}, which feature a \emph{univalence} axiom +that identifies isomorphisms between types with propositional equality. +For example we would have two isomorphisms, and thus two equalities, +between $\mybool$ and $\mybool$, corresponding to the two permutations---one is the identity, and one swaps the elements. Given this, $\myfun{K}$ and univalence are inconsistent, and thus a form of dependent pattern matching that does not imply $\myfun{K}$ is subject of @@ -1810,7 +1814,7 @@ framework we ought to be able to do the same: in the end, without considering the operational behaviour, all functions equal extensionally are going to be replaceable with one another. -However this is not the case, or in other words with the tools we have there is no closed term of type +However in ITT this is not the case, or in other words with the tools we have there is no closed term of type \[ \myfun{ext} : \myfora{\myb{A}\ \myb{B}}{\mytyp}{\myfora{\myb{f}\ \myb{g}}{ \myb{A} \myarr \myb{B}}{ @@ -1886,7 +1890,7 @@ Given these facts theories employing equality reflection, like NuPRL to keep the systems manageable. For all its faults, equality reflection does allow us to prove extensionality, -using the extensions we gave above. Assuming that $\myctx$ contains +using the extensions given in Section \ref{sec:extensions}. Assuming that $\myctx$ contains \[\myb{A}, \myb{B} : \mytyp; \myb{f}, \myb{g} : \myb{A} \myarr \myb{B}; \myb{q} : \myfora{\myb{x}}{\myb{A}}{\myapp{\myb{f}}{\myb{x}} \mypeq{} \myapp{\myb{g}}{\myb{x}}}\] We can then derive \begin{prooftree} @@ -1913,12 +1917,15 @@ A recent development by \citet{Altenkirch2007}, \emph{Observational Type Theory} (OTT), promises to keep the well behavedness of ITT while being able to gain many useful equality proofs,\footnote{It is suspected that OTT gains \emph{all} the equality proofs of ETT, but no proof - exists yet.} including function extensionality. The main idea is to -give the user the possibility to \emph{coerce} (or transport) values -from a type $\mytya$ to a type $\mytyb$, if the type checker can prove -structurally that $\mytya$ and $\mytyb$ are equal; and providing a -value-level equality based on similar principles. Here we give an -exposition which follows closely the original paper. + exists yet.} including function extensionality. The main idea is have +equalities to express structural properties of the equated terms, +instead of blindly comparing the syntax structure. In the case of +functions, this will correspond to extensionality, in the case of +products it will correspond to having equal projections, and so on. +Moreover, we are given a way to \emph{coerce} values from $\mytya$ to +$\mytyb$, if we can prove $\mytya$ equal to $\mytyb$, following similar +principles to the ones described above. Here we give an exposition +which follows closely the original paper. \subsection{A simpler theory, a propositional fragment} @@ -2020,10 +2027,11 @@ indeed we can `inject' any $\myprop$ back in $\mytyp$ with $\myprdec{\myarg}$. \end{tabular} } \\ Propositions are what we call the types of \emph{proofs}, or types - whose inhabitants contain no `data', much like $\myunit$. The goal - when isolating \mytyc{Prop} is twofold: erasing all top-level - propositions when compiling; and identifying all equivalent - propositions as the same, as we will see later. + whose inhabitants contain no `data', much like $\myunit$. Types of + these kind are called \emph{irrelevant}. Irrelevance can be exploited + in various ways---we can identify all equivalent proportions as + definitionally equal equal, as we will see later; and erase all the top + level propositions when compiling. Why did we choose what we have in $\myprop$? Given the above criteria, $\mytop$ obviously fits the bill, since it has one element. @@ -2120,23 +2128,23 @@ or `John Major', since John Major's `classless society' widened people's aspirations to equality, but also the gap between rich and poor. After all, aspiring to be equal to others than oneself is the politics of envy. In much - the same way, forms equations between members of any type, but they - cannot be treated as equals (ie substituted) unless they are of the - same type. Just as before, each thing is only equal to - itself. \citep{McBride1999}. + the same way, $\myjm{\myarg}{\myarg}{\myarg}{\myarg}$ forms equations + between members of any type, but they cannot be treated as equals (ie + substituted) unless they are of the same type. Just as before, each + thing is only equal to itself. \citep{McBride1999}. \end{quote} Correspondingly, at the term level, $\myfun{coe}$ (`coerce') lets us transport values between equal types; and $\myfun{coh}$ (`coherence') guarantees that $\myfun{coe}$ respects the value-level equality, or in -other words that it really has no computational component: if we +other words that it really has no computational component. If we transport $\mytmm : \mytya$ to $\mytmn : \mytyb$, $\mytmm$ and $\mytmn$ will still be the same. -Before introducing the core ideas that make OTT work, let us distinguish +Before introducing the core machinery of OTT work, let us distinguish between \emph{canonical} and \emph{neutral} terms and types. -\begin{mydef}[Canonical and neutral types and terms] +\begin{mydef}[Canonical and neutral terms and types] In a type theory, \emph{neutral} terms are those formed by an abstracted variable or by an eliminator (including function application). Everything else is \emph{canonical}. @@ -2161,20 +2169,20 @@ closed terms will reduce to a canonical term. The plan is to decompose type-level equalities between canonical types into decodable propositions containing equalities regarding the -subterms. So if are equating two product types, the equality will +subtypes. So if are equating two product types, the equality will reduce to two subequalities regarding the first and second type. Then, we can \myfun{coe}rce to transport values between equal types. -Following the subequalities, \myfun{coe} will procede recursively on the +Following the subequalities, \myfun{coe} will proceed recursively on the subterms. -This interplay between the canonicity of equated types, type -equalities, and \myfun{coe}, ensures that invocations of $\myfun{coe}$ -will vanish when we have evidence of the structural equality of the -types we are transporting terms across. If the type is neutral, the -equality will not reduce and thus $\myfun{coe}$ will not reduce either. -If we come across an equality between different canonical types, then we -reduce the equality to bottom, making sure that no such proof can exist, -and providing an `escape hatch' in $\myfun{coe}$. +This interplay between the canonicity of equated types, type equalities, +and \myfun{coe}, ensures that invocations of $\myfun{coe}$ will vanish +when we have evidence of the structural equality of the types we are +transporting terms across. If the type is neutral, the equality will +not reduce and thus $\myfun{coe}$ will not reduce either. If we come +across an equality between different canonical types, then we reduce the +equality to bottom, thus making sure that no such proof can exist, and +providing an `escape hatch' in $\myfun{coe}$. \begin{figure}[t] @@ -2262,8 +2270,8 @@ 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. +element of the proof 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 with some twists to make $\myfun{coe}$ work with the @@ -2272,7 +2280,7 @@ generated proofs; the reader can refer to the paper for details. \subsubsection{$\myfun{coe}$, laziness, and $\myfun{coh}$erence} \label{sec:lazy} -It is important to notice that in the reduction rules for $\myfun{coe}$ +It is important to notice that the reduction rules for $\myfun{coe}$ are never obstructed by the structure of the proofs. With the exception of comparisons between different canonical types we never `pattern match' on the proof pairs, but always look at the projections. This @@ -2337,13 +2345,13 @@ axioms as top-level abstracted variables. As with type-level equality, we want value-level equality to reduce based on the structure of the compared terms. When matching propositional data, such as $\myempty$ and $\myunit$, we automatically -return the trivial type, since if a type has zero one members, all +return the trivial type, since if a type has zero or one members, all members will be equal. When matching on data-bearing types, such as $\mybool$, we check that such data matches, and return bottom otherwise. When matching on records and functions, we rebuild the records to achieve $\eta$-expansion, and relate functions if they are extensionally equal---exactly what we wanted. The case for \mytyc{W} is omitted but -unsurprising, it checks that equal data in the nodes will bring equal +unsurprising, checking that equal data in the nodes will bring equal children. \subsection{Proof irrelevance and stuck coercions} @@ -2391,9 +2399,10 @@ exception is type holes, which we do not describe holes rigorously, but provide more information about them in Section \ref{sec:type-holes}. Note that in this section we will present \mykant\ terms in a fancy -\LaTeX\ dress too keep up with the presentation, but every term, with its -syntax reduced to the concrete syntax, is a valid \mykant\ term accepted -by \mykant\ the software, and not only \mykant\ the theory. Appendix +\LaTeX\ dress to keep up with the presentation, but every term, reduced +to its concrete syntax (which we will present in Section +\ref{sec:syntax}), is a valid \mykant\ term accepted by \mykant\ the +software, and not only \mykant\ the theory. Appendix \ref{app:kant-examples} displays most of the terms in this section in their concrete syntax. @@ -2431,14 +2440,14 @@ STLC. We will have two kinds of typing judgements: \emph{inference} and \emph{checking}. $\myinf{\mytmt}{\mytya}$ indicates that $\mytmt$ infers the type $\mytya$, while $\mychk{\mytmt}{\mytya}$ can be checked -against type $\mytya$. The arrows signify the direction of the type +against type $\mytya$. The arrows indicate the direction of the type checking---inference pushes types up, checking propagates types down. -The type of variables in context is inferred, and so are annotate terms. -The type of applications is inferred too, propagating types down the -applied term. Abstractions are checked. Finally, we have a rule to -check the type of an inferrable term. +The type of variables in context is inferred. The type of applications +and annotated terms is inferred too, propagating types down the applied +and annotated term, respectively. Abstractions are checked. Finally, +we have a rule to check the type of an inferrable term. \begin{mydef}[Bidirectional type checking for the STLC]\ \end{mydef} \mynegder @@ -2476,12 +2485,12 @@ naturals), we would have to annotate the term: \[ \begin{array}{@{}l} \myfun{comp} : (\mynat \myarr \mynat) \myarr (\mynat \myarr \mynat) \myarr \mynat \myarr \mynat \\ - \myfun{comp} \mapsto (\myabs{\myb{f}\, \myb{g}\, \myb{x}}{\myb{f}\myappsp(\myb{g}\myappsp\myb{x})}) + \myfun{comp} \myappsp \myb{f} \myappsp \myb{g} \myappsp \myb{x} \mapsto \myb{f}\myappsp(\myb{g}\myappsp\myb{x}) \end{array} \] But we would not have to annotate functions passed to it, since the type would be propagated to the arguments: \[ - \myfun{comp}\myappsp (\myabs{\myb{x}}{\myb{x} \mathrel{\myfun{$+$}} 3}) \myappsp (\myabs{\myb{x}}{\myb{x} \mathrel{\myfun{$*$}} 4}) \myappsp 42 : \mynat + \myfun{comp}\myappsp (\myabs{\myb{x}}{\myb{x} \mathrel{\myfun{$+$}} 3}) \myappsp (\myabs{\myb{x}}{\myb{x} \mathrel{\myfun{$*$}} 4}) \myappsp 42 \] \subsection{Base terms and types} @@ -2641,7 +2650,7 @@ although with some differences. \end{mydef} We denote term vectors with the usual arrow notation, -e.g. $vec{\mytmt}$, $\myvec{\mytmt};\mytmm$, etc. We often use term +e.g. $\vec{\mytmt}$, $\vec{\mytmt};\mytmm$, etc. We often use term vectors to refer to a series of term applied to another. For example $\mytyc{D} \myappsp \vec{A}$ is a shorthand for $\mytyc{D} \myappsp \mytya_1 \cdots \mytya_n$, for some $n$. $n$ is consistently used to @@ -3061,7 +3070,6 @@ $\mynat$---the type system is far too weak. \end{description} \begin{figure}[p] - \vspace{-.5cm} \mydesc{syntax}{ }{ \small $ @@ -4295,6 +4303,7 @@ implementation challenges present when implementing an interactive theorem prover. \subsection{Syntax} +\label{sec:syntax} The syntax of \mykant\ is presented in Figure \ref{fig:syntax}. Examples showing the usage of most of the constructs---excluding the @@ -4510,7 +4519,7 @@ inst t s = s >>= \v -> case v of The beauty of this technique is that with a few simple functions we have defined all the core operations in a general and `obviously correct' way, with the extra confidence of having the type checker looking our -back. For what concerns term equality, we can just ask the Haskell +back. For what concerns term equality, we can just ask the H Haskell compiler to derive the instance for the \verb|Eq| type class and since we are nameless that will be enough (modulo fancy quotation). @@ -4521,7 +4530,7 @@ also \cite{McBride2004b}. What are then the pitfalls of this seemingly invincible technique? The most obvious impediment is the need for polymorphic recursion. -Functions traversing terms parametrised by the variable type will have +Functions traversing terms parameterized by the variable type will have types such as \begin{Verbatim} -- Infer the type of a term, or return an error. @@ -4534,7 +4543,7 @@ undecidable \citep{henglein1993type}. This causes some annoyance, especially in the presence of many local definitions that we would like to leave untyped. -But the real issue is the fact that giving a type parametrised over a +But the real issue is the fact that giving a type parameterized over a variable---say \verb|m v|---a \verb|Monad| instance means being able to only substitute variables for values of type \verb|m v|. This is a considerable inconvenience. Consider for instance the case of @@ -4601,7 +4610,7 @@ and reduce further if it yields a new list of terms. This has the advantage of simplicity, at the expense of being quite poor in terms of performance and that we need to do quotation manually. An alternative that solves both of these is the already mentioned -\emph{normalization by evaluation}, where we would compute by turning +\emph{normalisation by evaluation}, where we would compute by turning terms into Haskell values, and then reify back to terms to compare them---a useful tutorial on this technique is given by \cite{Loh2010}. @@ -4613,7 +4622,7 @@ performance advantages can be rendered less effective by the continuous quoting and reifying, although this can probably be mitigated with some heuristics. -\subsubsection{Parametrise everything!} +\subsubsection{Parameterize everything!} \label{sec:parame} Through the life of a REPL cycle we need to execute two broad @@ -4645,14 +4654,14 @@ is,\footnote{See \url{https://en.wikibooks.org/wiki/Haskell/Monad_transformers.}} this is what \texttt{KMonadT} works with and provides: \begin{itemize} -\item The \verb|v| parameter represents the parametrised variable for +\item The \verb|v| parameter represents the parameterized variable for the term type that we spoke about at the beginning of this section. More on this later. \item The \verb|f| parameter indicates what kind of environment we are holding. Sometimes we want to traverse terms without carrying the entire environment, for various reasons---\texttt{KMonatT} lets us do - that. Note that \verb|f| is itself parametrised over \verb|v|. The + that. Note that \verb|f| is itself parameterized over \verb|v|. The inner \verb|StateT| monad transformer lets us retrieve and modify this environment at any time. @@ -4825,7 +4834,7 @@ in \ref{fig:graph-one-after}. \begin{mydef}[Strongly connected component] A \emph{strongly connected component} in a graph with vertices $V$ is a subset of $V$, say $V'$, such that for each $(v_1,v_2) \in V' \times - V$ there is a path from $v_1$ to $v_2$. + V'$ there is a path from $v_1$ to $v_2$. \end{mydef} The SCCs in the graph for the constraints above is shown in Figure @@ -4853,7 +4862,7 @@ constructs dear to the Haskell programmer. Keeping in mind the \texttt{KMonadT} monad described in Section \ref{sec:parame}, the REPL is represented as a function in \texttt{KMonadT} consuming input and hopefully producing output. Then, -frontends can very easily written by marshalling data in and out of the +front ends can very easily written by marshalling data in and out of the REPL: \begin{Verbatim} data Input @@ -4924,7 +4933,7 @@ then sends back a \texttt{JSON} message with the response. Moreover, each clien is handled in a separate threads, so crashes of the REPL for a certain client will not bring the whole application down. -On the frontend side, we had to write some JavaScript to accept input +On the front end side, we had to write some JavaScript to accept input from a form, and to make the responses appear on the screen. The web prompt is publicly available at \url{http://bertus.mazzo.li}, a sample session is shown Figure \ref{fig:web-prompt-one}. @@ -5330,7 +5339,7 @@ system that we described---here we review the main ones. Coinductive data types are the dual of this approach. We specify ways to destruct data, and we are given a way to generate the defined type - by repeatedly `unfolding' starting from some seed data. For example, + by repeatedly `unfolding' starting from some seed. For example, we could defined infinite streams by specifying a $\myfun{head}$ and $\myfun{tail}$ destructors---here using a syntax reminiscent of \mykant\ records: @@ -5719,7 +5728,7 @@ data Tm r v | Eq (Tm r v) (Tm r v) (Tm r v) (Tm r v) -- Either a data type, or a record. -data ADTRec = ADT | Rec +data ADTRec = ADT | Rc -- Either a coercion, or coherence. data Coeh = Coe | Coh\end{verbatim} @@ -5750,6 +5759,6 @@ efficiently with hash maps. \newpage{} \bibliographystyle{authordate1} -\bibliography{thesis} +\bibliography{final} \end{document} diff --git a/presentation.tex b/presentation.tex new file mode 100644 index 0000000..f3381bc --- /dev/null +++ b/presentation.tex @@ -0,0 +1,568 @@ +\documentclass{beamer} +\usepackage[sc,slantedGreek]{mathpazo} + + +% Comment these out if you don't want a slide with just the +% part/section/subsection/subsubsection title: +\AtBeginPart{\frame{\partpage}} +\AtBeginSection{\frame{\sectionpage}} +\AtBeginSubsection{\frame{\subsectionpage}} +\AtBeginSubsubsection{\frame{\subsubsectionpage}} +\beamertemplatenavigationsymbolsempty + +\setlength{\parindent}{0pt} +\setlength{\parskip}{6pt plus 2pt minus 1pt} +\setlength{\emergencystretch}{3em} % prevent overfull lines +\setcounter{secnumdepth}{0} + +\usepackage[english]{babel} +\usepackage[conor]{agda} +\renewcommand{\AgdaKeywordFontStyle}[1]{\ensuremath{\mathrm{\underline{#1}}}} +\renewcommand{\AgdaFunction}[1]{\textbf{\textcolor{AgdaFunction}{#1}}} +\renewcommand{\AgdaField}{\AgdaFunction} +% \definecolor{AgdaBound} {HTML}{000000} +\definecolor{AgdaHole} {HTML} {FFFF33} + +\DeclareUnicodeCharacter{9665}{\ensuremath{\lhd}} +\DeclareUnicodeCharacter{964}{\ensuremath{\tau}} +\DeclareUnicodeCharacter{963}{\ensuremath{\sigma}} +\DeclareUnicodeCharacter{915}{\ensuremath{\Gamma}} +\DeclareUnicodeCharacter{8799}{\ensuremath{\stackrel{?}{=}}} +\DeclareUnicodeCharacter{9655}{\ensuremath{\rhd}} + +\newcommand{\mysmall}{} +\newcommand{\mysyn}{\AgdaKeyword} +\newcommand{\mytyc}[1]{\textup{\AgdaDatatype{#1}}} +\newcommand{\mydc}[1]{\textup{\AgdaInductiveConstructor{#1}}} +\newcommand{\myfld}[1]{\textup{\AgdaField{#1}}} +\newcommand{\myfun}[1]{\textup{\AgdaFunction{#1}}} +\newcommand{\myb}[1]{\AgdaBound{$#1$}} +\newcommand{\myfield}{\AgdaField} +\newcommand{\myind}{\AgdaIndent} +\newcommand{\mykant}{\textmd{\textsc{Bertus}}} +\newcommand{\mysynel}[1]{#1} +\newcommand{\myse}{\mysynel} +\newcommand{\mytmsyn}{\langle t \rangle} +\newcommand{\mysp}{\ } +\newcommand{\myabs}[2]{\mydc{$\lambda$} #1 \mathrel{\mydc{$\mapsto$}} #2} +\newcommand{\myappsp}{\hspace{0.07cm}} +\newcommand{\myapp}[2]{#1 \myappsp #2} +\newcommand{\mysynsep}{\ \ |\ \ } +\newcommand{\myITE}[3]{\myfun{If}\, #1\, \myfun{Then}\, #2\, \myfun{Else}\, #3} +\newcommand{\mycumul}{\preceq} + +\newcommand{\mydesc}[3]{ + \noindent + \mbox{ + \parbox{\textwidth}{ + {\mysmall + \vspace{0.2cm} + \hfill \textup{\phantom{ygp}\textbf{#1}} $#2$ + \framebox[\textwidth]{ + \parbox{\textwidth}{ + \vspace{0.1cm} + \centering{ + #3 + } + \vspace{0.2cm} + } + } + \vspace{0.2cm} + } + } + } +} + +\newcommand{\mytmt}{\mysynel{t}} +\newcommand{\mytmm}{\mysynel{m}} +\newcommand{\mytmn}{\mysynel{n}} +\newcommand{\myred}{\leadsto} +\newcommand{\myredd}{\stackrel{*}{\leadsto}} +\newcommand{\myreddd}{\stackrel{*}{\reflectbox{$\leadsto$}}} +\newcommand{\mysub}[3]{#1[#3 / #2]} +\newcommand{\mytysyn}{\langle ty \rangle} +\newcommand{\mybasetys}{K} +\newcommand{\mybasety}[1]{B_{#1}} +\newcommand{\mytya}{\myse{A}} +\newcommand{\mytyb}{\myse{B}} +\newcommand{\mytycc}{\myse{C}} +\newcommand{\myarr}{\mathrel{\textcolor{AgdaDatatype}{\to}}} +\newcommand{\myprod}{\mathrel{\textcolor{AgdaDatatype}{\times}}} +\newcommand{\myctx}{\Gamma} +\newcommand{\myvalid}[1]{#1 \vdash \underline{\mathrm{valid}}} +\newcommand{\myjudd}[3]{#1 \vdash #2 : #3} +\newcommand{\myjud}[2]{\myjudd{\myctx}{#1}{#2}} +\newcommand{\myabss}[3]{\mydc{$\lambda$} #1 {:} #2 \mathrel{\mydc{$\mapsto$}} #3} +\newcommand{\mytt}{\mydc{$\langle\rangle$}} +\newcommand{\myunit}{\mytyc{Unit}} +\newcommand{\mypair}[2]{\mathopen{\mydc{$\langle$}}#1\mathpunct{\mydc{,}} #2\mathclose{\mydc{$\rangle$}}} +\newcommand{\myfst}{\myfld{fst}} +\newcommand{\mysnd}{\myfld{snd}} +\newcommand{\myconst}{\myse{c}} +\newcommand{\myemptyctx}{\varepsilon} +\newcommand{\myhole}{\AgdaHole} +\newcommand{\myfix}[3]{\mysyn{fix} \myappsp #1 {:} #2 \mapsto #3} +\newcommand{\mysum}{\mathbin{\textcolor{AgdaDatatype}{+}}} +\newcommand{\myleft}[1]{\mydc{left}_{#1}} +\newcommand{\myright}[1]{\mydc{right}_{#1}} +\newcommand{\myempty}{\mytyc{Empty}} +\newcommand{\mycase}[2]{\mathopen{\myfun{[}}#1\mathpunct{\myfun{,}} #2 \mathclose{\myfun{]}}} +\newcommand{\myabsurd}[1]{\myfun{absurd}_{#1}} +\newcommand{\myarg}{\_} +\newcommand{\myderivsp}{} +\newcommand{\myderivspp}{\vspace{0.3cm}} +\newcommand{\mytyp}{\mytyc{Type}} +\newcommand{\myneg}{\myfun{$\neg$}} +\newcommand{\myar}{\,} +\newcommand{\mybool}{\mytyc{Bool}} +\newcommand{\mytrue}{\mydc{true}} +\newcommand{\myfalse}{\mydc{false}} +\newcommand{\myitee}[5]{\myfun{if}\,#1 / {#2.#3}\,\myfun{then}\,#4\,\myfun{else}\,#5} +\newcommand{\mynat}{\mytyc{$\mathbb{N}$}} +\newcommand{\myrat}{\mytyc{$\mathbb{R}$}} +\newcommand{\myite}[3]{\myfun{if}\,#1\,\myfun{then}\,#2\,\myfun{else}\,#3} +\newcommand{\myfora}[3]{(#1 {:} #2) \myarr #3} +\newcommand{\myexi}[3]{(#1 {:} #2) \myprod #3} +\newcommand{\mypairr}[4]{\mathopen{\mydc{$\langle$}}#1\mathpunct{\mydc{,}} #4\mathclose{\mydc{$\rangle$}}_{#2{.}#3}} +\newcommand{\mynil}{\mydc{[]}} +\newcommand{\mycons}{\mathbin{\mydc{∷}}} +\newcommand{\myfoldr}{\myfun{foldr}} +\newcommand{\myw}[3]{\myapp{\myapp{\mytyc{W}}{(#1 {:} #2)}}{#3}} +\newcommand{\mynodee}{\mathbin{\mydc{$\lhd$}}} +\newcommand{\mynode}[2]{\mynodee_{#1.#2}} +\newcommand{\myrec}[4]{\myfun{rec}\,#1 / {#2.#3}\,\myfun{with}\,#4} +\newcommand{\mylub}{\sqcup} +\newcommand{\mydefeq}{\cong} +\newcommand{\myrefl}{\mydc{refl}} +\newcommand{\mypeq}{\mytyc{=}} +\newcommand{\myjeqq}{\myfun{$=$-elim}} +\newcommand{\myjeq}[3]{\myapp{\myapp{\myapp{\myjeqq}{#1}}{#2}}{#3}} +\newcommand{\mysubst}{\myfun{subst}} +\newcommand{\myprsyn}{\myse{prop}} +\newcommand{\myprdec}[1]{\mathopen{\mytyc{$\llbracket$}} #1 \mathclose{\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{\mytop}{\mytyc{$\top$}} +\newcommand{\mycoe}{\myfun{coe}} +\newcommand{\mycoee}[4]{\myapp{\myapp{\myapp{\myapp{\mycoe}{#1}}{#2}}{#3}}{#4}} +\newcommand{\mycoh}{\myfun{coh}} +\newcommand{\mycohh}[4]{\myapp{\myapp{\myapp{\myapp{\mycoh}{#1}}{#2}}{#3}}{#4}} +\newcommand{\myjm}[4]{(#1 {:} #2) \mathrel{\mytyc{=}} (#3 {:} #4)} +\newcommand{\myeq}{\mathrel{\mytyc{=}}} +\newcommand{\myprop}{\mytyc{Prop}} +\newcommand{\mytmup}{\mytmsyn\uparrow} +\newcommand{\mydefs}{\Delta} +\newcommand{\mynf}{\Downarrow} +\newcommand{\myinff}[3]{#1 \vdash #2 \Uparrow #3} +\newcommand{\myinf}[2]{\myinff{\myctx}{#1}{#2}} +\newcommand{\mychkk}[3]{#1 \vdash #2 \Downarrow #3} +\newcommand{\mychk}[2]{\mychkk{\myctx}{#1}{#2}} +\newcommand{\myann}[2]{#1 : #2} +\newcommand{\mydeclsyn}{\myse{decl}} +\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{\myelabt}{\vdash} +\newcommand{\myelabf}{\rhd} +\newcommand{\myelab}[2]{\myctx \myelabt #1 \myelabf #2} +\newcommand{\mytele}{\Delta} +\newcommand{\mytelee}{\delta} +\newcommand{\mydcctx}{\Gamma} +\newcommand{\mynamesyn}{\myse{name}} +\newcommand{\myvec}{\overrightarrow} +\newcommand{\mymeta}{\textsc} +\newcommand{\myhyps}{\mymeta{hyps}} +\newcommand{\mycc}{;} +\newcommand{\myemptytele}{\varepsilon} +\newcommand{\mymetagoes}{\Longrightarrow} +% \newcommand{\mytesctx}{\ +\newcommand{\mytelesyn}{\myse{telescope}} +\newcommand{\myrecs}{\mymeta{recs}} +\newcommand{\myle}{\mathrel{\lcfun{$\le$}}} +\newcommand{\mylet}{\mysyn{let}} +\newcommand{\myhead}{\mymeta{head}} +\newcommand{\mytake}{\mymeta{take}} +\newcommand{\myix}{\mymeta{ix}} +\newcommand{\myapply}{\mymeta{apply}} +\newcommand{\mydataty}{\mymeta{datatype}} +\newcommand{\myisreco}{\mymeta{record}} +\newcommand{\mydcsep}{\ |\ } +\newcommand{\mytree}{\mytyc{Tree}} +\newcommand{\myproj}[1]{\myfun{$\pi_{#1}$}} +\newcommand{\mysigma}{\mytyc{$\Sigma$}} +\newcommand{\mynegder}{\vspace{-0.3cm}} +\newcommand{\myquot}{\Uparrow} +\newcommand{\mynquot}{\, \Downarrow} +\newcommand{\mycanquot}{\ensuremath{\textsc{quote}{\Downarrow}}} +\newcommand{\myneuquot}{\ensuremath{\textsc{quote}{\Uparrow}}} +\newcommand{\mymetaguard}{\ |\ } +\newcommand{\mybox}{\Box} +\newcommand{\mytermi}[1]{\text{\texttt{#1}}} +\newcommand{\mysee}[1]{\langle\myse{#1}\rangle} +\newcommand{\mycomp}{\mathbin{\myfun{$\circ$}}} +\newcommand{\mylist}[1]{\mathopen{\mytyc{$[$}} #1 \mathclose{\mytyc{$]$}}} +\newcommand{\mylistt}[1]{\mathopen{\mydc{$[$}} #1 \mathclose{\mydc{$]$}}} +\newcommand{\myplus}{\mathbin{\myfun{$+$}}} +\newcommand{\mytimes}{\mathbin{\myfun{$*$}}} + +\renewcommand{\[}{\begin{equation*}} +\renewcommand{\]}{\end{equation*}} +\newcommand{\mymacol}[2]{\text{\textcolor{#1}{$#2$}}} + +\title{\mykant: Implementing Observational Equality} +\author{Francesco Mazzoli \texttt{}} +\date{June 2013} + +\begin{document} +\frame{\titlepage} + +\begin{frame} + \frametitle{Theorem provers are short-sighted} + + Two functions dear to the Haskell practitioner: + \[ + \begin{array}{@{}l} + \myfun{map} : (\myb{a} \myarr \myb{b}) \myarr \mylist{\myb{a}} \myarr \mylist{\myb{b}} \\ + \begin{array}{@{}l@{\myappsp}c@{\myappsp}c@{\ }c@{\ }l} + \myfun{map} & \myb{f} & \mynil & = & \mynil \\ + \myfun{map} & \myb{f} & (\myb{x} \mycons \myb{xs}) & = & \myapp{\myb{f}}{\myb{x}} \mycons \myfun{map} \myappsp \myb{f} \myappsp \myb{xs} \\ + \end{array} + \\ + \ \\ + (\myfun{${\circ}$}) : (\myb{b} \myarr \myb{c}) \myarr (\myb{a} \myarr \myb{b}) \myarr (\myb{a} \myarr \myb{c}) \\ + (\myb{f} \mathbin{\myfun{$\circ$}} \myb{g}) \myappsp \myb{x} = \myapp{\myb{g}}{(\myapp{\myb{f}}{\myb{x}})} + \end{array} + \] +\end{frame} + +\begin{frame} + \frametitle{Theorem provers are short-sighted} + $\myfun{map}$'s composition law states that: + \[ + \forall \myb{f} {:} (\myb{b} \myarr \myb{c}), \myb{g} {:} (\myb{a} \myarr \myb{b}). \myfun{map}\myappsp \myb{f} \mycomp \myfun{map}\myappsp \myb{g} \myeq \myfun{map}\myappsp (\myb{f} \mycomp \myb{g}) + \] + We can convince Coq or Agda that + \[ + \forall \myb{f} {:} (\myb{b} \myarr \myb{c}), \myb{g} {:} (\myb{a} \myarr \myb{b}), \myb{l} {:} \mylist{\myb{a}}. (\myfun{map}\myappsp \myb{f} \mycomp \myfun{map}\myappsp \myb{g}) \myappsp \myb{l} \myeq \myfun{map}\myappsp (\myb{f} \mycomp \myb{g}) \myappsp \myb{l} + \] + But we cannot get rid of the $\myb{l}$. Why? +\end{frame} + +\begin{frame} + \frametitle{Observational equality and \mykant} + + \emph{Observational equality} is a solution to this and other equality + annoyances. + + \mykant\ is a system making observational equality more usable. + + The theory of \mykant\ is complete, the practice, not quite. +\end{frame} + +\begin{frame} + \frametitle{Theorem provers, dependent types} First class types: we + can return them, have them as arguments, etc. + \[ + \begin{array}{@{}l@{\ }l@{\ \ \ }l} + \mysyn{data}\ \myempty & & \text{No members.} \\ + \mysyn{data}\ \myunit & = \mytt & \text{One member.} \\ + \mysyn{data}\ \mynat & = \mydc{zero} \mydcsep \mydc{suc}\myappsp\mynat & \text{Natural numbers.} + \end{array} + \] + $\myempty : \mytyp$, $\myunit : \mytyp$, $\mynat : \mytyp$. + + $\myunit$ is trivially inhabitable: it corresponds to $\top$ in + logic. + + $\myempty$ is \emph{not} inhabitable: it corresponds to $\bot$. + +\end{frame} + +\begin{frame} + \frametitle{Theorem provers, dependent types} + + We can express relations: + \[ + \begin{array}{@{}l} + (\myfun{${>}$}) : \mynat \myarr \mynat \myarr \mytyp \\ + \begin{array}{@{}c@{\,}c@{\,}c@{\ }l} + \mydc{zero} & \mathrel{\myfun{$>$}} & \myb{m} & = \myempty \\ + \myb{n} & \mathrel{\myfun{$>$}} & \mydc{zero} & = \myunit \\ + (\mydc{suc} \myappsp \myb{n}) & \mathrel{\myfun{$>$}} & (\mydc{suc} \myappsp \myb{m}) & = \myb{n} \mathrel{\myfun{$>$}} \myb{m} + \end{array} + \end{array} + \] + + A term of type $\myb{m} \mathrel{\myfun{$>$}} \myb{n}$ represents a + \emph{proof} that $\myb{n}$ is indeed greater than $\myb{n}$. + \[ + \begin{array}{@{}l} + 3 \mathrel{\myfun{$>$}} 1 \myred \myunit \\ + 2 \mathrel{\myfun{$>$}} 2 \myred \myempty \\ + 0 \mathrel{\myfun{$>$}} \myb{m} \myred \myempty + \end{array} + \] + + Thus, proving that $2 \mathrel{\myfun{$>$}} 2$ corresponds to proving + falsity, while $3 \mathrel{\myfun{$>$}} 1$ is fine. +\end{frame} + +\begin{frame} + \frametitle{Example: safe $\myfun{head}$ function} + + \[ + \begin{array}{@{}l} + \mysyn{data}\ \mylistt{\myb{A}} = \mynil \mydcsep \myb{A} \mycons \mylistt{\myb{A}} \\ + \ \\ + \myfun{length} : \mylistt{\myb{A}} \myarr \mynat \\ + \begin{array}{@{}l@{\myappsp}c@{\ }c@{\ }l} + \myfun{length} & \mynil & = & \mydc{zero} \\ + \myfun{length} & (\myb{x} \mycons \myb{xs}) & = & \mydc{suc} \myappsp (\myfun{length} \myappsp \myb{xs}) + \end{array} \\ + \ \\ + \myfun{head} : \myfora{\myb{l}}{\mytyc{List}\myappsp\myb{A}}{ \myfun{length}\myappsp\myb{l} \mathrel{\myfun{$>$}} 0 \myarr \myb{A}} \\ + \begin{array}{@{}l@{\myappsp}c@{\myappsp}c@{\ }c@{\ }l} + \myfun{head} & \mynil & \myb{p} & = & \myhole{?} \\ + \myfun{head} & (\myb{x} \mycons \myb{xs}) & \myb{p} & = & \myb{x} + \end{array} + \end{array} + \] + + The type of $\myb{p}$ in the $\myhole{?}$ is $\myempty$, since + \[\myfun{length} \myappsp \mynil \mathrel{\myfun{$>$}} 0 \myred 0 \mathrel{\myfun{$>$}} 0 \myred \myempty \] +\end{frame} + + +\begin{frame} + \frametitle{Example: safe $\myfun{head}$ function} + + \[ + \begin{array}{@{}l} + \mysyn{data}\ \mylistt{\myb{A}} = \mynil \mydcsep \myb{A} \mycons \mylistt{\myb{A}} \\ + \ \\ + \myfun{length} : \mytyc{List}\myappsp\myb{A} \myarr \mynat \\ + \begin{array}{@{}l@{\myappsp}c@{\ }c@{\ }l} + \myfun{length} & \mynil & = & \mydc{zero} \\ + \myfun{length} & (\myb{x} \mycons \myb{xs}) & = & \mydc{suc} \myappsp (\myfun{length} \myappsp \myb{xs}) + \end{array} \\ + \ \\ + \myfun{head} : \myfora{\myb{l}}{\mytyc{List}\myappsp\myb{A}}{ \myfun{length}\myappsp\myb{l} \mathrel{\myfun{$>$}} 0 \myarr \myb{A}} \\ + \begin{array}{@{}l@{\myappsp}c@{\myappsp}c@{\ }c@{\ }l} + \myfun{head} & \mynil & \myb{p} & = & \myabsurd \myappsp \myb{p} \\ + \myfun{head} & (\myb{x} \mycons \myb{xs}) & \myb{p} & = & \myb{x} + \end{array} + \end{array} + \] + + Where $\myfun{absurd}$ corresponds to the logical \emph{ex falso + quodlibet}---given $\myempty$, we can get anything: + \[ + \myfun{absurd} : \myempty \myarr \myb{A} + \] +\end{frame} + +\begin{frame} + \frametitle{How do we type check this thing?} + \[ + \myfun{head} \myappsp \mylistt{3} : \myfun{length} \myappsp \mylistt{3} \mathrel{\myfun{$>$}} 0 \myarr \mynat + \] + + Will $\mytt : \myunit$ do as an argument? In other words, when type + checking, do we have that + \[ + \begin{array}{@{}c@{\ }c@{\ }c} + \myunit & \mydefeq & \myfun{length} \myappsp \mylistt{3} \mathrel{\myfun{$>$}} 0 \\ + \myfun{length} \myappsp \mynil \mathrel{\myfun{$>$}} 0 & \mydefeq & \myempty \\ + (\myabs{\myb{x}\, \myb{y}}{\myb{y}}) \myappsp \myunit \myappsp \myappsp \mynat & \mydefeq & (\myabs{\myb{x}\, \myb{y}}{\myb{x}}) \myappsp \mynat \myappsp \myunit \\ + & \vdots & + \end{array} + \] + ? +\end{frame} + +\begin{frame} + \frametitle{Definitional equality} + + The type checker needs a notion of equality between types. + + We reduce terms `as far as possible' (to their \emph{normal form}) and + then compare them syntactically: + \[ + \begin{array}{@{}r@{\ }c@{\ }c@{\ }c@{\ }c@{\ }c@{\ }l} + \myunit & \myredd & \myunit & \mydefeq & \myunit & \myreddd & \myfun{length} \myappsp \mylistt{3} \mathrel{\myfun{$>$}} 0 \\ + \myfun{length} \myappsp \mynil \mathrel{\myfun{$>$}} 0 & \myredd & \myempty & \mydefeq & \myempty & \myreddd & \myempty \\ + (\myabs{\myb{x}\, \myb{y}}{\myb{y}}) \myappsp \myunit \myappsp \myappsp \mynat & \myredd & \mynat & \mydefeq & \mynat & \myreddd & (\myabs{\myb{x}\, \myb{y}}{\myb{x}}) \myappsp \mynat \myappsp \myunit \\ + & & & \vdots & & & + \end{array} + \] + + This equality, $\mydefeq$, takes the name of \emph{definitional} equality. +\end{frame} + +\begin{frame} + \frametitle{Propositional equality} Using definitional equality, we + can give the user a type-level notion of term equality. + \[ + (\myeq) : \myb{A} \myarr \myb{A} \myarr \mytyp + \] + We introduce members of $\myeq$ by reflexivity: + \[ + \myrefl\myappsp\mytmt : \mytmt \myeq \mytmt + \] + So that $\myrefl$ will relate definitionally equal terms: + \[ + \myrefl\myappsp 5 : (3 + 2) \myeq (1 + 4)\ \text{since}\ (3 + 2) \myeq (1 + 4) \myredd 5 \myeq 5 + \] + Then we can use a substitution law to derive other + laws---transitivity, congruence, etc. +\end{frame} + +\begin{frame} +\frametitle{The problem with prop. equality} +Going back to $\myfun{map}$, we can prove that +\[ \forall \myb{f} {:} (\myb{b} \myarr \myb{c}), \myb{g} {:} (\myb{a} \myarr \myb{b}), \myb{l} {:} \mylist{\myb{a}}. (\myfun{map}\myappsp \myb{f} \mycomp \myfun{map}\myappsp \myb{g}) \myappsp \myb{l} \myeq \myfun{map}\myappsp (\myb{f} \mycomp \myb{g}) \myappsp \myb{l} \] +Because we can prove, by induction on $\myb{l}$, that we will always get definitionally equal lists. + +But without the $\myb{l}$, we cannot compute, so we are stuck with +\[ +\myfun{map}\myappsp \myb{f} \mycomp \myfun{map}\myappsp \myb{g} \not\mydefeq \myfun{map}\myappsp (\myb{f} \mycomp \myb{g}) +\] +\end{frame} + +\begin{frame} + \frametitle{The solution} + + \emph{Observational} equality, instead of basing its equality on + definitional equality, looks at the structure of the type to decide: + \[ + \begin{array}{@{}l} + (\myfun{map}\myappsp \myb{f} \mycomp \myfun{map}\myappsp \myb{g} : \mylistt{\myb{A_1}} \myarr \mylistt{\myb{C_1}}) \myeq (\myfun{map}\myappsp (\myb{f} \mycomp \myb{g}) : \mylistt{\myb{A_2}} \myarr \mylistt{\myb{C_2}}) \myred \\ + \myind{2} (\myb{l_1} : \myb{A_1}) \myarr (\myb{l_2} : \myb{A_2}) \myarr (\myb{l_1} : \myb{A_1}) \myeq (\myb{l_2} : \myb{A_2}) \myarr \\ + \myind{2} ((\myfun{map}\myappsp \myb{f} \mycomp \myfun{map}\myappsp \myb{g}) \myappsp \myb{l} : \mylistt{\myb{C_1}}) \myeq (\myfun{map}\myappsp (\myb{f} \mycomp \myb{g}) \myappsp \myb{l} : \mylistt{\myb{C_2}}) + \end{array} + \] + This extends to other structures (tuples, inductive types, \dots). + Moreover, if we can deem two \emph{types} equal, we can \emph{coerce} + values from one to the other. +\end{frame} + +\begin{frame} + \frametitle{\mykant} + + Observational equality was described in a very restricted theory. + + \mykant\ aims to incorporate it in a more `practical' environment, + where we have: + \begin{itemize} + \item User defined data types (inductive data and records). + \item A type hierarchy. + \item Partial type inference (bidirectional type checking). + \item Type holes. + \end{itemize} +\end{frame} + +\begin{frame} + \frametitle{Inductive data} + Good old Haskell data types: + \[ + \mysyn{data}\ \mytyc{List}\myappsp \myb{A} = \mynil \mydcsep \myb{A} \mycons \mytyc{List}\myappsp\myb{A} + \] + But instead of general recursion and pattern matching, we have + structural induction: + \[ + \begin{array}{@{}l@{\ }l} + \mytyc{List}.\myfun{elim} : & (\myb{P} : \mytyc{List}\myappsp\myb{A} \myarr \mytyp) \myarr \\ + & \myb{P} \myappsp \mynil \myarr \\ + & ((\myb{x} : \myb{A}) \myarr (\myb{l} : \mytyc{List}\myappsp \myb{A}) \myarr \myb{P} \myappsp \myb{l} \myarr \myb{P} \myappsp (\myb{x} \mycons \myb{l})) \myarr \\ + & (\myb{l} : \mytyc{List}\myappsp\myb{A}) \myarr \myb{P} \myappsp \myb{l} + \end{array} + \] + Reduction: + \[ + \begin{array}{@{}l@{\ }l} + \mytyc{List}.\myfun{elim} \myappsp \myse{P} \myappsp \myse{pn} \myappsp \myse{pc} \myappsp \mynil & \myred \myse{pn} \\ + \mytyc{List}.\myfun{elim} \myappsp \myse{P} \myappsp \myse{pn} \myappsp \myse{pc} \myappsp (\mytmm \mycons \mytmn) & \myred \myse{pc} \myappsp \mytmm \myappsp \mytmn \myappsp (\mytyc{List}.\myfun{elim} \myappsp \myse{P} \myappsp \myse{pn} \myappsp \myse{ps} \myappsp \mytmt ) + \end{array} + \] +\end{frame} + +\begin{frame} + \frametitle{Records} + But also records: + \[ + \mysyn{record}\ \mytyc{Tuple}\myappsp\myb{A}\myappsp\myb{B} = \mydc{tuple}\ \{ \myfun{fst} : \myb{A}, \myfun{snd} : \myb{B} \} + \] + Where each field defines a projection from instances of the record: + \[ + \begin{array}{@{}l@{\ }c@{\ }l} + \myfun{fst} & : & \mytyc{Tuple}\myappsp\myb{A}\myappsp\myb{B} \myarr \myb{A} \\ + \myfun{snd} & : & \mytyc{Tuple}\myappsp\myb{A}\myappsp\myb{B} \myarr \myb{B} + \end{array} + \] + Where the projection's reduction rules are predictably + \[ + \begin{array}{@{}l@{\ }l} + \myfun{fst}\myappsp&(\mydc{tuple}\myappsp\mytmm\myappsp\mytmn) \myred \mytmm \\ + \myfun{snd}\myappsp&(\mydc{tuple}\myappsp\mytmm\myappsp\mytmn) \myred \mytmn \\ + \end{array} + \] +\end{frame} + +\begin{frame} + \frametitle{Dependend defined types} \emph{Unlike} Haskell, we can + have fields of a data constructor to depend on earlier fields: + \[ + \begin{array}{@{}l} + \mysyn{record}\ \mytyc{Tuple}\myappsp(\myb{A} : \mytyp)\myappsp(\myb{B} : \myb{A} \myarr \mytyp) = \\ + \myind{2}\mydc{tuple}\ \{ \myfun{fst} : \myb{A}, \myfun{snd} : \myb{B}\myappsp\myb{fst} \} + \end{array} + \] + $\mytyc{Tuple}$ takes a $\mytyp$, $\myb{A}$, and a predicate from + elements of $\myb{A}$ to types, $\myb{B}$. + + This way, the \emph{type} of the second element depends on the + \emph{value} of the first: + \[ + \begin{array}{@{}l@{\ }l} + \myfun{fst} & : \mytyc{Tuple}\myappsp\myb{A}\myappsp\myb{B} \myarr \myb{A} \\ + \myfun{snd} & : (\myb{x} : \mytyc{Tuple}\myappsp\myb{A}\myappsp\myb{B}) \myarr \myb{B} \myappsp (\myfun{fst} \myappsp \myb{x}) + \end{array} + \] +\end{frame} + +\begin{frame} + \frametitle{Type hierarchy} + Up to now, we have thrown $\mytyp$ around, as `the type of types'. + + But what is the type of $\mytyp$ itself? The simple way out is + \[ + \mytyp : \mytyp + \] + This solution is not only simple, but inconsistent, for the same + reason that the notion of a `powerset' in na{\"i}ve set theory is. + + Instead, following Russell, we shall have + \[ + \{\mynat, \mybool, \mytyc{List}\myappsp\mynat, \cdots\} : \mytyp_0 : \mytyp_1 : \cdots + \] + We talk of types in $\mytyp_0$ as `smaller' than types in $\mytyp_1$. +\end{frame} + +\begin{frame} + \frametitle{Cumulativity and typical ambiguity} + Is it OK to take + \[ \mytyp_0 : \mytyp_2 \] + ? +\end{frame} + +\begin{frame} +\begin{center} +{\Huge Questions?} +\end{center} +\end{frame} + +\end{document} -- 2.30.2