From: Francesco Mazzoli Date: Sat, 5 Jan 2013 14:56:49 +0000 (+0000) Subject: more background report X-Git-Url: https://git.enpas.org/?p=bitonic-mengthesis.git;a=commitdiff_plain;h=df8c324f993e70dacfb248d8a22a05f895fa5465 more background report --- diff --git a/docs/background.tex b/docs/background.tex index 507dbf8..ff4e8cd 100644 --- a/docs/background.tex +++ b/docs/background.tex @@ -82,6 +82,8 @@ \maketitle +\setlength{\tabcolsep}{12pt} + The marriage between programming and logic has been a very fertile one. In particular, since the simply typed lambda calculus (STLC), a number of type systems have been devised with increasing expressive power. @@ -110,41 +112,50 @@ abstractions, and applications: \newcommand{\appspace}{\hspace{0.07cm}} \newcommand{\app}[2]{#1\appspace#2} -\newcommand{\abs}[2]{\lambda #1. #2} -\newcommand{\termt}{\mathrm{T}} -\newcommand{\termm}{\mathrm{M}} -\newcommand{\termn}{\mathrm{N}} -\newcommand{\termp}{\mathrm{P}} -\newcommand{\separ}{\ |\ } +\newcommand{\absspace}{\hspace{0.03cm}} +\newcommand{\abs}[2]{\lambda #1\absspace.\absspace#2} +\newcommand{\termt}{t} +\newcommand{\termm}{m} +\newcommand{\termn}{n} +\newcommand{\termp}{p} +\newcommand{\termf}{f} +\newcommand{\separ}{\ \ |\ \ } +\newcommand{\termsyn}{\mathit{term}} +\newcommand{\axname}[1]{\textbf{#1}} +\newcommand{\axdesc}[2]{\axname{#1} \fbox{$#2$}} +\begin{center} +\axname{syntax} \begin{eqnarray*} - \termt & ::= & x \separ (\abs{x}{\termt}) \separ (\app{\termt}{\termt}) \\ - x & \in & \text{Some enumerable set of symbols, e.g.}\ \{x, y, z, \dots , x_1, x_2, \dots\} + \termsyn & ::= & x \separ (\abs{x}{\termsyn}) \separ (\app{\termsyn}{\termsyn}) \\ + x & \in & \text{Some enumerable set of symbols, e.g.}\ \{x, y, z, \dots , x_1, x_2, \dots\} \end{eqnarray*} +\end{center} + % I will omit parethesis in the usual manner. %TODO explain how -Intuitively, abstractions ($\abs{x}{\termt}$) introduce functions with a named -parameter ($x$), and applications ($\app{\termt}{\termm}$) apply a function -($\termt$) to an argument ($\termm$). +I will use $\termt,\termm,\termn,\dots$ to indicate a generic term, and $x,y$ +for variables. I will also assume that all variable names in a term are unique +to avoid problems with name capturing. Intuitively, abstractions +($\abs{x}{\termt}$) introduce functions with a named parameter ($x$), and +applications ($\app{\termt}{\termm}$) apply a function ($\termt$) to an argument +($\termm$). The ``applying'' is more formally explained with a reduction rule: -\newcommand{\bred}{\to_{\beta}} +\newcommand{\bred}{\leadsto} +\newcommand{\bredc}{\bred^*} -\begin{eqnarray*} - \app{(\abs{x}{\termt})}{\termm} & \bred & \termt[\termm / x] \\ - \termt \bred \termm & \Rightarrow & \left \{ - \begin{array}{l} - \app{\termt}{\termn} \bred \app{\termm}{\termn} \\ - \app{\termn}{\termt} \bred \app{\termn}{\termm} \\ - \abs{x}{\termt} \bred \abs{x}{\termm} - \end{array} - \right. -\end{eqnarray*} +\begin{center} +\axdesc{reduction}{\termsyn \bred \termsyn} +$$\app{(\abs{x}{\termt})}{\termm} \bred \termt[\termm / x]$$ +\end{center} Where $\termt[\termm / x]$ expresses the operation that substitutes all -occurrences of $x$ with $\termm$ in $\termt$. +occurrences of $x$ with $\termm$ in $\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. % % TODO put the trans closure @@ -161,9 +172,9 @@ material analysed. \subsection{The simply typed $\lambda$-calculus} -\newcommand{\tya}{\mathrm{A}} -\newcommand{\tyb}{\mathrm{B}} -\newcommand{\tyc}{\mathrm{C}} +\newcommand{\tya}{A} +\newcommand{\tyb}{B} +\newcommand{\tyc}{C} 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. @@ -174,53 +185,63 @@ reads ``in context $\Gamma$, term $\termt$ has type $\tya$''. The syntax for types is as follows: \newcommand{\tyarr}{\to} +\newcommand{\tysyn}{\mathit{type}} +\newcommand{\ctxsyn}{\mathit{context}} +\newcommand{\emptyctx}{\cdot} -\begin{equation*} - \tya ::= x \separ \tya \tyarr \tya -\end{equation*} +\begin{center} + \axname{syntax} + $$\tysyn ::= x \separ \tysyn \tyarr \tysyn$$ +\end{center} -The $x$ represents all the primitive types that we might want to add to our -calculus, for example $\mathbb{N}$ or $\mathsf{Bool}$. +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. Note that, being a map, no variable can -appear twice as a subject in a context. +$\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 types\footnote{Actually, we don't need to: computers can infer the right type easily, but that is another story.}: -\begin{equation*} - \termt ::= \dots \separ (\abs{x : \tya}{\termt}) -\end{equation*} +\begin{center} + \axname{syntax} + $$\termsyn ::= x \separ (\abs{x : \tysyn}{\termsyn}) \separ (\app{\termsyn}{\termsyn})$$ +\end{center} Now we are ready to give the typing judgements: \begin{center} - \begin{prooftree} + \axdesc{typing}{\Gamma \vdash \termsyn : \tysyn} + + \vspace{0.5cm} + + \begin{tabular}{c c c} \AxiomC{} - \UnaryInfC{$\Gamma, x : \tya \vdash x : \tya$} - \end{prooftree} - \begin{prooftree} - \AxiomC{$\Gamma, x : \tya \vdash \termt : \tyb$} + \UnaryInfC{$\Gamma; x : \tya \vdash x : \tya$} + \DisplayProof + & + \AxiomC{$\Gamma; x : \tya \vdash \termt : \tyb$} \UnaryInfC{$\Gamma \vdash \abs{x : \tya}{\termt} : \tya \tyarr \tyb$} - \end{prooftree} - \begin{prooftree} + \DisplayProof + \end{tabular} + + \vspace{0.5cm} + + \begin{tabular}{c} \AxiomC{$\Gamma \vdash \termt : \tya \tyarr \tyb$} \AxiomC{$\Gamma \vdash \termm : \tya$} \BinaryInfC{$\Gamma \vdash \app{\termt}{\termm} : \tyb$} - \end{prooftree} + \DisplayProof + \end{tabular} \end{center} 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} - % TODO the definition of "stuck" thing is wrong -\item[Progress] A well-typed term is not stuck. With stuck, we mean a compound - term (not a variable or a value) that cannot be reduced further. In the raw - $\lambda$-calculus all we have is functions, but if we add other primitive - types and constructors it's easy to see how things can go bad - for example - trying to apply a boolean to something. +\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 + 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 resulting term is also well typed. \end{description} @@ -232,34 +253,37 @@ give types to the non-normalising term shown before: \app{(\abs{x : ?}{\app{x}{x}})}{(\abs{x : ?}{\app{x}{x}})} \end{equation*} -\newcommand{\lcfix}[2]{\mathsf{fix} \appspace #1. #2} +\newcommand{\lcfix}[2]{\mathsf{fix} \appspace #1\absspace.\absspace #2} This makes the STLC Turing incomplete. We can recover the ability to loop by adding a combinator that recurses: \begin{equation*} - \termt ::= \dots \separ \lcfix{x : \tya}{\termt} -\end{equation*} -\begin{equation*} - \lcfix{x : \tya}{\termt} \bred \termt[(\lcfix{x : \tya}{\termt}) / x] + \termsyn ::= \dots \separ \lcfix{x : \tysyn}{\termsyn} \end{equation*} \begin{center} \begin{prooftree} - \AxiomC{$\Gamma,x : \tya \vdash \termt : \tya$} + \AxiomC{$\Gamma;x : \tya \vdash \termt : \tya$} \UnaryInfC{$\Gamma \vdash \lcfix{x : \tya}{\termt} : \tya$} \end{prooftree} \end{center} +\begin{equation*} + \lcfix{x : \tya}{\termt} \bred \termt[(\lcfix{x : \tya}{\termt}) / x] +\end{equation*} However, we will keep STLC without such a facility. In the next section we shall see why that is preferable for our needs. \subsection{The Curry-Howard correspondence} +\label{sec:curry-howard} + +\newcommand{\lcunit}{\mathsf{()}} It turns out that the STLC can be seen a natural deduction system. Terms are proofs, and their types are the propositions they prove. This remarkable fact -is known as the Curry-Howard isomorphism. +is known as the Curry-Howard correspondence, or isomorphism. The ``arrow'' ($\to$) type corresponds to implication. If we wished to -prove that $(\tya \tyarr \tyb) \tyarr (\tyb \tyarr \tyc) \tyarr (\tyc +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: \begin{equation*} @@ -268,9 +292,10 @@ correct type: That is, function composition. We might want extend our bare lambda calculus with a couple of terms to make our natural deduction more pleasant to use. For example, tagged unions (\texttt{Either} in Haskell) are disjunctions, and tuples -are conjunctions. We also want to be able to express falsity, and that is done -by introducing a type inhabited by no terms. If evidence of such a type is -presented, then we can derive any type, which expresses absurdity. +(or products) are conjunctions. We also want to be able to express falsity, and +that is done by introducing a type inhabited by no terms. If evidence of such a +type is presented, then we can derive any type, which expresses absurdity. +Conversely, $\top$ is the type with just one trivial element, $\lcunit$. \newcommand{\lcinl}{\mathsf{inl}\appspace} \newcommand{\lcinr}{\mathsf{inr}\appspace} @@ -286,21 +311,18 @@ presented, then we can derive any type, which expresses absurdity. \newcommand{\botel}{\bot E} \newcommand{\lcabsurd}{\mathsf{absurd}\appspace} -\begin{eqnarray*} - \termt & ::= & \dots \\ - & | & \lcinl \termt \separ \lcinr \termt \separ \lccase{\termt}{\termt}{\termt} \\ - & | & (\termt , \termt) \separ \lcfst \termt \separ \lcsnd \termt -\end{eqnarray*} -\begin{eqnarray*} - \lccase{(\lcinl \termt)}{\termm}{\termn} & \bred & \app{\termm}{\termt} \\ - \lccase{(\lcinr \termt)}{\termm}{\termn} & \bred & \app{\termn}{\termt} \\ - \lcfst (\termt , \termm) & \bred & \termt \\ - \lcsnd (\termt , \termm) & \bred & \termm -\end{eqnarray*} -\begin{equation*} - \tya ::= \dots \separ \tya \vee \tya \separ \tya \wedge \tya \separ \bot -\end{equation*} \begin{center} + \axname{syntax} + \begin{eqnarray*} + \termsyn & ::= & \dots \\ + & | & \lcinl \termsyn \separ \lcinr \termsyn \separ \lccase{\termsyn}{\termsyn}{\termsyn} \\ + & | & (\termsyn , \termsyn) \separ \lcfst \termsyn \separ \lcsnd \termsyn \\ + & | & \lcunit \\ + \tysyn & ::= & \dots \separ \tysyn \vee \tysyn \separ \tysyn \wedge \tysyn \separ \bot \separ \top + \end{eqnarray*} +\end{center} +\begin{center} + \axdesc{typing}{\Gamma \vdash \termsyn : \tysyn} \begin{prooftree} \AxiomC{$\Gamma \vdash \termt : \tya$} \RightLabel{$\orint$} @@ -315,43 +337,74 @@ presented, then we can derive any type, which expresses absurdity. \RightLabel{$\orel$} \TrinaryInfC{$\Gamma \vdash \lccase{\termt}{\termm}{\termn} : \tyc$} \end{prooftree} - \begin{prooftree} + + \begin{tabular}{c c} \AxiomC{$\Gamma \vdash \termt : \tya$} \AxiomC{$\Gamma \vdash \termm : \tyb$} \RightLabel{$\andint$} \BinaryInfC{$\Gamma \vdash (\tya , \tyb) : \tya \wedge \tyb$} - \end{prooftree} - \begin{prooftree} + \DisplayProof + & \AxiomC{$\Gamma \vdash \termt : \tya \wedge \tyb$} \RightLabel{$\andel$} \UnaryInfC{$\Gamma \vdash \lcfst \termt : \tya$} \noLine \UnaryInfC{$\Gamma \vdash \lcsnd \termt : \tyb$} - \end{prooftree} - \begin{prooftree} + \DisplayProof + \end{tabular} + + \vspace{0.5cm} + + \begin{tabular}{c c} \AxiomC{$\Gamma \vdash \termt : \bot$} \RightLabel{$\botel$} \UnaryInfC{$\Gamma \vdash \lcabsurd \termt : \tya$} - \end{prooftree} + \DisplayProof + & + \AxiomC{} + \RightLabel{$\top I$} + \UnaryInfC{$\Gamma \vdash \lcunit : \top$} + \DisplayProof + \end{tabular} +\end{center} +\begin{center} + \axdesc{reduction}{\termsyn \bred \termsyn} + \begin{eqnarray*} + \lccase{(\lcinl \termt)}{\termm}{\termn} & \bred & \app{\termm}{\termt} \\ + \lccase{(\lcinr \termt)}{\termm}{\termn} & \bred & \app{\termn}{\termt} \\ + \lcfst (\termt , \termm) & \bred & \termt \\ + \lcsnd (\termt , \termm) & \bred & \termm + \end{eqnarray*} \end{center} With these rules, our STLC now looks remarkably similar in power and use to the natural deduction we already know. $\neg A$ can be expressed as $A \tyarr \bot$. However, there is an important omission: there is no term of the type $A \vee \neg A$ (excluded middle), or equivalently $\neg \neg A \tyarr A$ (double -negation). +negation), or indeed any term with a type equivalent to those. This has a considerable effect on our logic and it's no coincidence, since there is no obvious computational behaviour for laws like the excluded middle. Theories of this kind are called \emph{intuitionistic}, or \emph{constructive}, and all the systems analysed will have this characteristic since they build on -the foundation of the STLC. +the foundation of the STLC\footnote{There is research to give computational + behaviour to classical logic, but we will not touch those subjects.}. + +Finally, going back to our $\mathsf{fix}$ combinator, it's now easy to see how +we would want to exclude such a thing if we want to use STLC as a logic, since +it allows us to prove everything: $(\lcfix{x : \tya}{x}) : \tya$ clearly works +for any $A$! This is a crucial point: in general we wish to have systems that +do not let the user devise a term of type $\bot$, otherwise our logic will be +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{\lcbool}{\mathsf{Bool}} +\newcommand{\lcforallz}[2]{\forall #1 \absspace.\absspace #2} +\newcommand{\lcforall}[3]{\forall #1 : #2 \absspace.\absspace #3} +\newcommand{\lcexists}[3]{\exists #1 : #2 \absspace.\absspace #3} The STLC can be made more expressive in various ways. Henk Barendregt succinctly expressed geometrically how we can expand our type system: @@ -375,17 +428,15 @@ Here $\lambda{\to}$, in the bottom left, is the STLC. From there can move along 3 dimensions: \begin{description} \item[Terms depending on types (towards $\lambda{2}$)] In other words, we can - quantify over types in our type signatures: $(\lambda A : \lctype. \lambda x : - A. x) : \forall A. A \to A$. The first and most famous instance of this idea + quantify over types in our type signatures: $(\abs{A : \lctype}{\abs{x : A}{x}}) : \lcforallz{A}{A \tyarr A}$. The first and most famous instance of this idea has been System F. This gives us a form of polymorphism and has been wildly successful, also thanks to a well known inference algorithm for a restricted version of System F known as Hindley-Milner. Languages like Haskell and SML are based on this discipline. \item[Types depending on types (towards $\lambda{\underline{\omega}}$)] In other - words, we have type operators: $(\lambda A : \lctype. \lambda R : \lctype. (A \to R) \to R) : \lctype \to \lctype \to \lctype$. + 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: $(\lambda x : - \lcbool. \lcite{x}{\mathbb{N}}{\mathbb{Q}}) : \lcbool \to \lctype$. + 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 @@ -395,6 +446,179 @@ where $\lambda{C}$ sits in the ``$\lambda$-cube'' above. \section{Intuitionistic Type Theory} -In this section I will describe +Intuitionistic Type Theory (ITT) is a very expressive system first described by +Per Martin-L\"{o}f at the end of the 70s. It extends the STLC giving it all the +properties described above, while retaining good computational properties. Here +we will present a core type theory and illustrate its components and properties +one by one, and then describe the various additions that make it useful as a +programming language and as a theorem prover. + +\newcommand{\lcset}[1]{\mathsf{Type}_{#1}} +\newcommand{\lcsetz}{\mathsf{Type}} +\newcommand{\defeq}{\equiv} + +\begin{center} + \axname{syntax} + \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 \\ + & | & \lcset{n} \\ + n & \in & \mathbb{N} + \end{eqnarray*} + + \axdesc{typing}{\Gamma \vdash \termsyn : \termsyn} + + \vspace{0.5cm} + + \begin{tabular}{c c c} + \AxiomC{} + \RightLabel{var} + \UnaryInfC{$\Gamma;x : \tya \vdash x : \tya$} + \DisplayProof + & + \AxiomC{$\Gamma \vdash \termt : \bot$} + \RightLabel{$\bot E$} + \UnaryInfC{$\Gamma \vdash \lcabsurd \termt : A$} + \DisplayProof + & + \AxiomC{$\Gamma \vdash \termt : \tya$} + \AxiomC{$\tya \defeq \tyb$} + \RightLabel{$\defeq$ type} + \BinaryInfC{$\Gamma \vdash \termt : \tyb$} + \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}$} + \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]$} + \DisplayProof + \end{tabular} + + \vspace{0.5cm} + + \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}$} + \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]$} + \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}$} + \noLine + \UnaryInfC{$\Gamma \vdash \lcexists{x}{\tya}{\tyb} : \lcset{n \sqcup m}$} + \DisplayProof + \end{tabular} + + \vspace{0.5cm} + + \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 + \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 terms and types are kept well separated (terms never go +``right of the colon''), in ITT types can freely depend on terms. + +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. + +$\forall$ and $\exists$ are at the core of the machinery of ITT: + +\begin{description} +\item[$\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 an interpretation of + functions as infinitary products. We will just call it ``dependent function'', + reserving ``product'' for $\exists$. + +\item[$\exists$] is a generalisation of $\wedge$ in the extended STLC of section + \ref{sec:curry-howard}, and thus we will call it ``dependent product''. 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 + interpretation of $\exists$ as a generalised $\vee$, where the 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 +create functions that accept and return types. For this reason we $\defeq$ as +the smallest + +\begin{thebibliography}{9} + +\bibitem{levitation} + James Chapman, Pierre-Evariste Dagand, Conor McBride, and Peter Morris. + \emph{The gentle art of levitation}. + SIGPLAN Not., 45:3–14, September 2010. + +\bibitem{outsidein} + Dimitrios Vytiniotis, Simon Peyton Jones, Tom Schrijvers, and Martin + Sulzmann. + \emph{OutsideIn(X): Modular Type inference with local assumptions}. + Journal of Functional Programming, 21, 2011. + +\bibitem{haskell-promotion} + Brent A. Yorgey, Stephanie Weirich, Julien Cretin, Simon Peyton Jones, + Dimitrios Vytiniotis, and Jos\'{e} Pedro Magalh\~{a}es. + \emph{Giving Haskell a promotion}. + In Proceedings of the 8th ACM SIGPLAN Workshop on Types in Language Design and + Implementation, TLDI ’12, pages 53–66, New York, NY, USA, 2012. ACM. doi: + 10.1145/2103786.2103795. + +\bibitem{idris} + Edwin Brady. + \emph{Implementing General Purpose Dependently Typed Programming Languages}. + Unpublished draft. + +\bibitem{bidirectional} + Benjamin C. Pierce and David N. Turner. + \emph{Local type inference}. + ACM Transactions on Programming Languages and Systems, 22(1):1–44, January + 2000. ISSN 0164-0925. doi: 10.1145/345099.345100. + +\end{thebibliography} \end{document}