1\section{The Core Type Theory}
3High level \Idris{} programs, as described in Section \ref{sect:hll}, are
4\remph{elaborated} to a small core language, \TT{}, then type checked.
5\TT{} is a dependently typed $\lambda$-calculus with inductive families
6and pattern matching definitions similar to UTT~\cite{luo1994}, and building
7on an earlier implementation, \Ivor{}~\cite{Brady2006b}.
9core language as small as is reasonably possible, which has several advantages: it is
10easy to type check, since type checking dependent type theory is well understood
11~\cite{loh2010tutorial}; and it is easy to transform, optimise and compile. Keeping
12the core language small increases our confidence that these important components of
13the language are correct. In this section, we describe \TT{} and
16\subsection{\TT{} syntax}
18The syntax of \TT{} expressions is given in Figure \ref{ttsyn}. This defines:
21\item \demph{Terms}, $\vt$, which are variables, bindings, applications or constants.
22\item \demph{Bindings}, $\vb$, which are lambda abstractions, let bindings, or function spaces.
23\item \demph{Constants}, $\vc$, which are integer or string literals, or $\Type_i$, the
27We may also write the function space $\all{\vx}{\vS}\SC\vT$ as $(\vx\Hab\vS)\to\vT$,
28or $\vS\to\vT$ if $\vx$ is not free in $\vT$, to make the notation more consistent with
29the high level language. Universe levels on sets ($\Type_i$) may be left implicit and
30inferred by the machine~\cite{pollack1990implicit}.
33\begin{array}{rll@{\hg}rll}
34\vt ::= & \vc & (\mbox{constants}) &
35\hg\vb ::= & \lam{\vx}{\vt} & (\mbox{abstraction}) \\
37 \mid & \vx & (\mbox{variable}) &
38 \mid & \LET\:\vx\defq\vt\Hab\vt & (\mbox{let binding}) \\
40 \mid & \vb\SC\:\vt & (\mbox{binding}) &
41 \mid & \all{\vx}{\vt} & (\mbox{function space}) \\
43 \mid & \vt\:\vt & (\mbox{application}) &
44% \mid & \pat{\vx}{\vt} & (\mbox{pattern variable}) \\
46% \mid & \pty{\vx}{\vt} & (\mbox{pattern type}) \\
48 \vc ::= & \Type_i & (\mbox{type universes}) \\
49 \mid & \vi & (\mbox{integer literal}) \\
50 \mid & \VV{str} & (\mbox{string literal}) \\
53{\TT{} expression syntax}
56A \TT{} program is a collection of \demph{inductive family} definitions (Section
57\ref{sect:inductivefams}) and \demph{pattern matching} function definitions (Section
58\ref{sect:patdefs}), as well as primitive operators on constants.
59Before defining these, let us define the semantics of \TT{}
62\subsection{\TT{} semantics}
64The static and dynamic semantics of \TT{} are defined mutually, since
65evaluation relies on a well-typed term, and type checking relies on
66evaluation. Everything is defined relative
67to a context, $\Gamma$. The empty context
68is valid, as is a context extended with a $\lambda$, $\forall$ or
72\Axiom{\proves\RW{valid}}
74\Rule{\Gamma\proves\RW{valid}}
75{\Gamma;\vb\proves\RW{valid}}
78\subsubsection{Evaluation}
80\label{sect:evaluation}
82Evaluation of \TT{} is defined by contraction schemes, given in Figure
83\ref{ttcontract}. \demph{Contraction}, relative to a context $\Gamma$, is given
84by one of the following schemes:
87\item $\beta$-contraction, which substitutes a value applied to a $\lambda$-binding for
88the bound variable. We define $\beta$-constraction simply by replacing the $\lambda$-binding
90\item $\delta$-contraction, which replaces a $\LET$ bound variable with its value.
93\demph{Reduction} ($\reduces$) is the structural closure of contraction, and evaluation
94is ($\reducesto$) is the transitive closure of reduction. \demph{Conversion} ($\converts$)
95is the smallest equivalence relation closed under reduction. If $\Gamma\proves\vx\converts\vy$
96then $\vy$ can be obtained from $\vx$ by a finite, possibly empty, sequence of
97contractions and reversed contractions. Terms which are convertible are also said to
98be computationally equal.
99The evaluator can also be extended by defining pattern matching functions, which
100will be described in more detail in Section \ref{sect:patdefs}. In principle, pattern
101matching functions can be understood as extending the core language with high level
106\beta\mathrm{-contraction} &
108\Gamma\proves(\lam{\vx}{\vS}\SC\vt)\:\vs\leadsto\LET\:\vx\defq\vs\Hab\vS\SC\vt
110\delta\mathrm{-contraction} &
112\Gamma;\LET\:\vx\defq\vs\Hab\vS;\Gamma'
118{\TT{} contraction schemes}
123\subsubsection{Typing rules}
125\label{sect:typerules}
127The type inference rules for \TT{} expressions are given in Figure \ref{typerules}.
128These rules use the \demph{cumulativity} relation, defined in
129Figure \ref{cumul}. The type of types, $\Type_i$ is parameterised by a universe level,
130to prevent Girard's paradox~\cite{coquand1986analysis}. Cumulativity allows programs at
131lower universe levels to inhabit higher universe levels. In practice, universe levels
132can be left implicit (and will be left implicit in the rest of this paper) ---
133the type checker generates a graph of constraints between universe levels (such
134as that produced by the $\mathsf{Forall}$ typing rule) and checks that there
135are no cycles. Otherwise, the typing rules are standard and type inference can
136be implemented in the usual way~\cite{loh2010tutorial}.
138\FFIG{\begin{array}{c}
140\Rule{\Gamma\proves\RW{valid}}
141{\Gamma\vdash\Type_n\Hab\Type_{n+1}}
144\Rule{(\lam{\vx}{\vS})\in\Gamma}
145{\Gamma\vdash\vx\Hab\vS}
148\Rule{(\all{\vx}{\vS})\in\Gamma}
149{\Gamma\vdash\vx\Hab\vS}
152\Rule{(\LET\:\vx\Hab\vS\defq\vs)\in\Gamma}
153{\Gamma\vdash\vx\Hab\vS}
156%\Rule{(\pat{\vx}{\vS})\in\Gamma}
157%{\Gamma\vdash\vx\Hab\vS}
160%\Rule{(\pty{\vx}{\vS})\in\Gamma}
161%{\Gamma\vdash\vx\Hab\vS}
164\Rule{\Gamma\vdash\vf\Hab\fbind{\vx}{\vS}{\vT}\hg\Gamma\vdash\vs\Hab\vS}
165{\Gamma\vdash\vf\:\vs\Hab\vT[\vs/\vx]} % \LET\:\vx\Hab\vS\:\defq\:\vs\:\IN\:\vT}
168\Rule{\Gamma;\lam{\vx}{\vS}\vdash\ve\Hab\vT\hg\Gamma\proves\fbind{\vx}{\vS}{\vT}\Hab\Type_n}
169{\Gamma\vdash\lam{\vx}{\vS}.\ve\Hab\fbind{\vx}{\vS}{\vT}}
172\Rule{\Gamma;\all{\vx}{\vS}\vdash\vT\Hab\Type_m\hg\Gamma\vdash\vS\Hab\Type_n}
173{\Gamma\vdash\fbind{\vx}{\vS}{\vT}\Hab\Type_p}
174\:(\exists\vp.\vm\le\vp,\:\vn\le\vp)
177\Rule{\begin{array}{c}\Gamma\proves\ve_1\Hab\vS\hg
178 \Gamma;\LET\:\vx\defq\ve_1\Hab\vS\proves\ve_2\Hab\vT\\
179 \Gamma\proves\vS\Hab\Type_n\hg
180 \Gamma;\LET\:\vx\defq\ve_1\Hab\vS\proves\vT\Hab\Type_n\end{array}
182{\Gamma\vdash\LET\:\vx\defq\ve_1\Hab\vS\SC\:\ve_2\Hab
184%\Let\:\vx\Hab\vS\defq\ve_1\:\IN\:\vT}
188\Rule{\Gamma\proves\vx\Hab\vA\hg\Gamma\proves\vA'\Hab\Type_n\hg
189 \Gamma\proves\vA\cumul\vA'}
190 {\Gamma\proves\vx\Hab\vA'}
193{Typing rules for \TT{}}
198\Rule{\Gamma\proves\vS\converts\vT}
199{\Gamma\proves\vS\cumul\vT}
201\Axiom{\Gamma\proves\Type_n\cumul\Type_{n+1}}
203\Rule{\Gamma\proves\vR\cumul\vS\hg\Gamma\proves\vS\cumul\vT}
204{\Gamma\proves\vR\cumul\vT}
206\Rule{\Gamma\proves\vS_1\converts\vS_2\hg\Gamma;\vx\Hab\vS_1\proves\vT_1\cumul\vT_2}
207{\Gamma\proves\all{\vx}{\vS_1}\SC\vT_1\cumul\all{\vx}{\vS_2}{\vT_2}}
213\subsection{Inductive Families}
215\label{sect:inductivefams}
217Inductive families \cite{dybjer1994inductive} are a form of simultaneously
218defined collection of algebraic data types which can be parametrised over
219\remph{values} as well as types. An inductive family is declared
220in a similar style to a Haskell GADT declaration~\cite{pj2006gadts}
222follows, using the de Bruijn telescope notation, $\tx$, to indicate a
223sequence of zero or more $\vx$:
227\Data\hg\TC{T}\:(\tx\Hab\ttt)\Hab\vt\hg\Where\hg
228\DC{c}_1\Hab\vt\:\mid\:\ldots\:\mid\:\DC{c}_n\Hab\vt
232Constructors may take recursive arguments in the family
233$\TC{T}$. Furthermore these arguments may themselves be indexed by another type ---
234if such indices do not involve $\TC{T}$ then the constructor is
235\demph{strictly positive}, which ensures that recursive arguments of the
236constructor are structurally smaller than the value itself.
238For example, the \Idris{} data type \tTC{Nat} would be declared in \TT{} as follows:
241\Data\hg\Nat\Hab\Type\hg\Where\hg\Z\Hab\Nat\:\mid\:\suc\Hab\fbind{\vk}{\Nat}{\Nat}
244A data type may have zero or more parameters (which are invariant
245across a structure) and a number of indices, given by the type. For
246example, the \TT{} equivalent of \tTC{List} is parametrised over its element type:
250\Data\hg\List\:(\va\Hab\Type)\Hab\Type\hg\Where
252& \nil\Hab\List\:\va\\
253\mid & (\cons)\Hab\fbind{\vx}{\va}{\fbind{\vxs}{\List\:\va}{\List\:\va}}
259parametrised over values. Using this, we can declare the type of
260vectors (lists with length), where the empty list is statically known
261to have length zero, and the non empty list is statically known to
262have a non zero length. The \TT{} equivalent of \tTC{Vect} is parametrised over its element type,
263like $\List$, but \remph{indexed} over its length. Note also that the length
264index $\vk$ is given \remph{explicitly}.
268\Data\hg\Vect\:(\va\Hab\Type)\Hab\Nat\to\Type\hg\Where \\
270& \nil\Hab\Vect\:\va\:\Z\\
271\mid & (\cons)\Hab\fbind{\vk}{\Nat}{
272\fbind{\vx}{\va}{\fbind{\vxs}{\Vect\:\va\:\vk}{\Vect\:\va\:(\suc\:\vk)}}
278\subsection{Pattern matching definitions}
282\subsubsection{Syntax}
284A pattern matching definition for a function named $\FN{f}$ takes the following form,
285consisting of a type declaration followed by one or more pattern clauses:
290\pat{\tx_1}{\ttt_1}\SC\FN{f}\:\ttt_1\:=\:\vt_1\\
292\pat{\tx_n}{\ttt_n}\SC\FN{f}\:\ttt_n\:=\:\vt_n\\
296A pattern clause consists of a list of pattern variable bindings,
297and a left and right hand side, both of which
298are \TT{} expressions. Each side is type checked relative to the variable bindings,
299and the types of each side must convert. Additionally, the
300left hand side must take the form of $\FN{f}$ applied to a number of \TT{} expressions,
301and the number of arguments must be the same in each clause. The right hand
302sides may include applications of $\FN{f}$, i.e. pattern matching definitions may
303be recursive. Termination analysis is implemented separately. The validity of a pattern
304clause is defined by the following rule:
308\Gamma;\lam{\tx}{\tU}\proves\FN{f}\:\tts\Hab\vS\hg
309\Gamma;\lam{\tx}{\tU}\proves\ve\Hab\vT\hg
310\Gamma\proves\vS\converts\vT}
312\Gamma\proves\pat{\tx}{\tU}\SC\FN{f}\:\tts\:=\:\ve\:\RW{valid}
316A valid pattern matching definition effectively extends \TT{} with a new constant,
317with the given type (extending the initial typing rules given in Section \ref{sect:typerules})
318and reduction behaviour (extending the initial reduction rules given in Section
319\ref{sect:evaluation}).
321\subsubsection{Semantics}
323Matching on an expression proceeds by comparing the expression to
324each match clause in order, resulting in either:
327\item \demph{Success}, with pattern variables mapping to expressions
328\item \demph{Failure}, with matching continuing by proceeding to the next match clause
329\item Matching being \demph{blocked}, for example by attempting to match a variable
330against a constructor pattern. In this case, no reduction occurs, because instantiating
331the variable may provide enough information for the clause to match.
334% Pat(x args) => x (Pat' args)
338In order to implement pattern matching, we must separate the \remph{accessible} and
339\remph{inaccessible} patterns. A pattern is \demph{accessible} (that is, it is possible
340to match against it) if it is constructor headed, or a variable. Inaccessible patterns
341are converted to ``match anything'' patterns. We convert clauses to matchable pattern
342clauses with the $\MO{Clause}$ operation, given in Figure \ref{mkclause}.
343We extend the telescope notation to meta-operations: the notation $\vec{\MO{Pat}}$ lifts the
344$\MO{Pat}$ operation across a list of arguments.
349& \MO{Clause} & (\pat{\tx}{\tU}\SC\FN{f}\:\tts\:=\:\ve)
350 & \MoRet{\FN{f}\:(\vec{\MO{Pat}}\:\tts)\:=\:\ve}
354& \MO{Pat} & (\vx\:\tts) & \MoRet{\vx\:(\vec{\MO{Pat}}\:\tts)
355 \hg\mbox{(if $\MO{Con}\:\vx$ and $\MO{Arity}\:\vx = \MO{Length}\:\tts$)}} \\
356& \MO{Pat} & \vx & \MoRet{\vx} \hg\mbox(if $\vx$ is a pattern variable)\\
357& \MO{Pat} & \cdot & \MoRet{\_} \hg\mbox(in all other cases)\\
361{Building matchable pattern clauses}
365% Match (c args, c args') => Match' (args, args')
366% Match (c args, x) => Blocked
367% Match (x, t) => Success (x => t)
368% Match (_, t) => Success ()
370\newcommand{\Blocked}{\mathsf{Blocked}}
371\newcommand{\Success}{\mathsf{Success}}
372\newcommand{\Failure}{\mathsf{Failure}}
374Pattern matching is invoked by the evaluator on encountering a function with
375a pattern matching definition applied to some arguments. If successful, pattern
376matching returns a new expression, which can then be reduced further.
377Figure \ref{pmatch} gives the semantics of pattern matching a collection of
379$\tc$ against an expression $\ve$. $\MO{Match}$ attempts to match each clause in
380turn against $\ve$. If matching a clause returns $\Success$ or $\Blocked$, then
381matching terminates. If matching a clause returns $\Failure$, then matching proceeds
382with the next clause. The algorithm uses the following meta-operations:
385\item $\MO{Con}\:\vx$, which returns true if $\vx$ is a constructor name
386\item $\MO{Arity}\:\vx$, which, if $\vx$ is a constructor name, returns the number of arguments
388\item $\MO{Length}\:\tts$, which returns the length of the telescope $\tts$
395& \MO{MatchArg} & (\vx\:\tts) & (\vx\:\tts')
396 & \MoRet{\vec{\MO{MatchArg}}\:\tts\:\tts'\hg\mbox{(if $\MO{Con}\:\vx$)}}\\
397& \MO{MatchArg} & (\vx\:\tts) & \vx & \MoRet{\Blocked} \\
398& \MO{MatchArg} & \vx & \vt & \MoRet{\Success\:(\vx\mapsto\vt)} \\
399& \MO{MatchArg} & \_ & \vt & \MoRet{\Success\:()} \\
400& \MO{MatchArg} & \cdot & \cdot & \MoRet{\Failure}
404& \MO{MatchClause} & (\vf\:\tp = \ve) & (\vf\:\tts) &
407 \Success\:\ve[\tx/\tv]\hg\mbox{(if $\vec{\MO{MatchArg}}\:\tp\:\tts \mq \Success\:(\tx,\tv)$)}\\
408 \Blocked\hg\mbox{(if $\vec{\MO{MatchArg}}\:\tp\:\tts \mq \Blocked$)}\\
409 \Failure\hg\mbox{(if $\vec{\MO{MatchArg}}\:\tp\:\tts \mq \Failure$)}\\
412& \MO{MatchClause} & (\vf\:\tp = \ve) & \cdot & \MoRet{\Failure} \\
416& \MO{Match} & (\vc ; \tc) & \ve &
419 \Success\:\vx\hg\mbox{(if $\MO{MatchClause}\:\vc\:\ve \mq \Success\:\vx)$} \\
420 \Blocked\hg\mbox{(if $\MO{MatchClause}\:\vc\:\ve \mq \Blocked)$} \\
421 \MO{Match}\:\tc\:\ve\hg\mbox{(otherwise)}
424& \MO{Match} & \cdot & \ve & \MoRet{\Failure}
428{Pattern matching semantics}
431In practice, for efficiency, pattern matching is implemented by compiling the match clauses to
432a tree of case expressions~\cite{Augustsson1985}.
434\subsection{From \Idris{} to \TT{}}
436\TT{} is a very small language, consisting only of data declarations and pattern matching
437function definitions. There is no significant innovation in the design of \TT{}, and this
438is a deliberate choice --- it is a combination of small, well-understood components.
439The kernel of the \TT{} implementation, consisting of a type checker, evaluator and
440pattern match compiler, is less than 1000 lines of Haskell code. If we are confident
441in the correctness of the kernel of \TT{}, and any higher level language feature
442can be translated into \TT{}, we can be more confident of the correctness of the high
443level language implementation that if it were implemented directly.
445The process of elaborating a high level language into a core type theory like \TT{} is,
446however, less well understood, and presents several challenges depending on the
447features of the high level language.
448%Elaboration has been implemented in various different ways,
449%for example in Agda~\cite{norell2007thesis} and Epigram~\cite{McBride2004a}.
451\subsubsection{Example Elaboration}
453Consider the following \Idris{} function:
455\begin{SaveVerbatim}{vadd}
457vAdd : Num a => Vect a n -> Vect a n -> Vect a n
459vAdd (x :: xs) (y :: ys) = x + y :: vAdd xs ys
465This adds corresponding elements of vectors of the same length. The vectors can contain
466any numeric type, overloaded using the \texttt{Num} type class. In order to elaborate
467this to \TT{}, we must resolve the implicit arguments, and make the type class explicit.
469The first step is to make the implicit arguments explicit, using a placeholder
470to stand for the arguments we have not yet resolved. The type class argument is
471also treated as an implicit argument, to which we give the name \texttt{c}:
473\begin{SaveVerbatim}{vAddImp}
475vAdd : (a : _) -> (n : _) -> Num a -> Vect a n -> Vect a n -> Vect a n
476vAdd _ _ c (Nil _) (Nil _) = (Nil _)
477vAdd _ _ c ((::) _ _ x xs) ((::) _ _ y ys)
478 = (::) _ _ ((+) _ x y) (vAdd _ _ _ xs ys)
483Next, we resolve the implicit arguments. Each implicit argument can only take
484one value for this program to be type correct --- these are solved by a unification
487\begin{SaveVerbatim}{vAddImpSolve}
489vAdd : (a : Set) -> (n : Nat) -> Num a -> Vect a n -> Vect a n -> Vect a n
490vAdd a O c (Nil a) (Nil a) = Nil a
491vAdd a (S k) c ((::) a k x xs) ((::) a k y ys)
492 = (::) a k ((+) c x y) (vAdd a k c xs ys)
495\useverb{vAddImpSolve}
497Finally, to build the \TT{} definition, we need to find the type of each pattern variable
498and state it explicitly. This leads to the \TT{} definition in Figure \ref{ttvadd},
499switching to \TT{} notation from the ASCII \Idris{} syntax.
504\FN{vAdd} & \Hab(\va\Hab\Set)\to(\vn\Hab\Nat)\to\TC{Num}\:\va\to
505 \Vect\:\va\:\vn\to\Vect\:\va\:\vn\to\Vect\:\va\:\vn\\
508\begin{array}{lccccccc}
510\RW{var}\:\va\Hab\Set,\:\vc\Hab\TC{Num}\;\va\SC}\\
511\hg\FN{vAdd} & \va & \Z & \vc & (\DC{Nil}\;\va) & (\DC{Nil}\;\va) & \Ret{\DC{Nil}\;\va} \\
514\va\Hab\Set,\:\vk\Hab\Nat,\;\vc\Hab\TC{Num}\;\va,\\
515\vx\Hab\va,\;\vxs\Hab\Vect\;\va\;\vk,\;
516\vy\Hab\va,\;\vys\Hab\Vect\;\va\;\vk
520\hg\FN{vAdd} & \va & (\suc\;\vk) & \vc
521 & ((\DC{::})\;\va\;\vk\;\vx\;\vxs)
522 & ((\DC{::})\;\va\;\vk\;\vy\;\vys)
524 & & \MRet{5}{((\DC{::})\;\va\;\vk\;((+)\;\vc\;\vx\;\vy)\; (\FN{vAdd}\;\va\;\vk\;\vc\;\vxs\;\vys))}
528{Pairwise addition of vectors in \TT{}}
531\subsubsection{An observation}
533\Idris{} programs may contain several high level constructs not present in \TT{}, such
534as implicit arguments, type classes, \texttt{where} clauses, pattern matching \texttt{let}
535and \texttt{case} constructs. We would like the high level language to be as expressive
536as possible, while remaining possible to translate to \TT{}.
538Before considering how to achieve this, we make an observation about the distinction between
539programming and theorem proving with dependent types, and appropriate mechanisms for
540constructing programs and theorems:
543\item \remph{Pattern matching} is a convenient abstraction for humans to write programs,
544in that it allows a programmer to express exactly the computational behaviour of a function.
545\item \remph{Tactics}, such as those used in the Coq theorem prover~\cite{Bertot2004},
546are a convenient abstraction for building proofs and programs by \remph{refinement}.
549The idea behind the \Idris{} elaborator, therefore, is to use the high level program
550to direct \demph{tactics} to build \TT{} programs by refinement. We implement the
551elaborator as an Embedded Domain Specific Language (EDSL) in Haskell.
553of this paper, we decribe the EDSL, and demonstrate how it can be used to implement
554all of the high level features of \Idris{}.
keysesc to close
- j k
- move down, up
- enter
- open
- esc
- back, or up a level
- 1 2 3 4
- readme, files, commits, refs
- /
- filter
- y
- copy the clone command
- c
- compare the chosen commit with another (or shift-click both)
- ?
- show or hide this list