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{constant}) &
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$-contraction simply by replacing the $\lambda$-binding
90\item $\delta$-contraction, which replaces a $\LET$ bound variable with its value.
94We use the following contextual closure rule to reduce a $\LET$ binding by creating
95a $\delta$-reducible expression:
98\Rule{\Gamma;\LET\:\vx\defq\vs\proves\vt\leadsto\vu}
99{\Gamma\proves\LET\:\vx\defq\vs\Hab\vS\SC\vt\leadsto\vu}
102\demph{Reduction} ($\reduces$) is the structural closure of contraction, and evaluation
103is ($\reducesto$) is the transitive closure of reduction. \demph{Conversion} ($\converts$)
104is the smallest equivalence relation closed under reduction. If $\Gamma\proves\vx\converts\vy$
105then $\vy$ can be obtained from $\vx$ by a finite, possibly empty, sequence of
106contractions and reversed contractions. Terms which are convertible are also said to
107be computationally equal.
108The evaluator can also be extended by defining pattern matching functions, which
109will be described in more detail in Section \ref{sect:patdefs}. In principle, pattern
110matching functions can be understood as extending the core language with high level
115\beta\mathrm{-contraction} &
117\Gamma\proves(\lam{\vx}{\vS}\SC\vt)\:\vs\leadsto\LET\:\vx\defq\vs\Hab\vS\SC\vt
119\delta\mathrm{-contraction} &
121\Gamma;\LET\:\vx\defq\vs\Hab\vS;\Gamma'
127{\TT{} contraction schemes}
132\subsubsection{Typing rules}
134\label{sect:typerules}
136The type inference rules for \TT{} expressions are given in Figure \ref{typerules}.
137These rules use the \demph{cumulativity} relation, defined in
138Figure \ref{cumul}. The type of types, $\Type_i$ is parameterised by a universe level,
139to prevent Girard's paradox~\cite{coquand1986analysis}. Cumulativity allows programs at
140lower universe levels to inhabit higher universe levels. In practice, universe levels
141can be left implicit (and will be left implicit in the rest of this paper) ---
142the type checker generates a graph of constraints between universe levels (such
143as that produced by the $\mathsf{Forall}$ typing rule) and checks that there
144are no cycles. Otherwise, the typing rules are standard and type inference can
145be implemented in the usual way~\cite{loh2010tutorial}.
147\FFIG{\begin{array}{c}
149\Rule{\Gamma\proves\RW{valid}}
150{\Gamma\vdash\Type_n\Hab\Type_{n+1}}
153\Rule{(\lam{\vx}{\vS})\in\Gamma}
154{\Gamma\vdash\vx\Hab\vS}
157\Rule{(\all{\vx}{\vS})\in\Gamma}
158{\Gamma\vdash\vx\Hab\vS}
161\Rule{(\LET\:\vx\Hab\vS\defq\vs)\in\Gamma}
162{\Gamma\vdash\vx\Hab\vS}
165%\Rule{(\pat{\vx}{\vS})\in\Gamma}
166%{\Gamma\vdash\vx\Hab\vS}
169%\Rule{(\pty{\vx}{\vS})\in\Gamma}
170%{\Gamma\vdash\vx\Hab\vS}
173\Rule{\Gamma\vdash\vf\Hab\fbind{\vx}{\vS}{\vT}\hg\Gamma\vdash\vs\Hab\vS}
174{\Gamma\vdash\vf\:\vs\Hab\vT[\vs/\vx]} % \LET\:\vx\Hab\vS\:\defq\:\vs\:\IN\:\vT}
177\Rule{\Gamma;\lam{\vx}{\vS}\vdash\ve\Hab\vT\hg\Gamma\proves\fbind{\vx}{\vS}{\vT}\Hab\Type_n}
178{\Gamma\vdash\lam{\vx}{\vS}.\ve\Hab\fbind{\vx}{\vS}{\vT}}
181\Rule{\Gamma;\all{\vx}{\vS}\vdash\vT\Hab\Type_m\hg\Gamma\vdash\vS\Hab\Type_n}
182{\Gamma\vdash\fbind{\vx}{\vS}{\vT}\Hab\Type_p}
183\:(\exists\vp.\vm\le\vp,\:\vn\le\vp)
186\Rule{\begin{array}{c}\Gamma\proves\ve_1\Hab\vS\hg
187 \Gamma;\LET\:\vx\defq\ve_1\Hab\vS\proves\ve_2\Hab\vT\\
188 \Gamma\proves\vS\Hab\Type_n\hg
189 \Gamma;\LET\:\vx\defq\ve_1\Hab\vS\proves\vT\Hab\Type_n\end{array}
191{\Gamma\vdash\LET\:\vx\defq\ve_1\Hab\vS\SC\:\ve_2\Hab
193%\Let\:\vx\Hab\vS\defq\ve_1\:\IN\:\vT}
197\Rule{\Gamma\proves\vx\Hab\vA\hg\Gamma\proves\vA'\Hab\Type_n\hg
198 \Gamma\proves\vA\cumul\vA'}
199 {\Gamma\proves\vx\Hab\vA'}
202{Typing rules for \TT{}}
207\Rule{\Gamma\proves\vS\converts\vT}
208{\Gamma\proves\vS\cumul\vT}
210\Axiom{\Gamma\proves\Type_n\cumul\Type_{n+1}}
212\Rule{\Gamma\proves\vR\cumul\vS\hg\Gamma\proves\vS\cumul\vT}
213{\Gamma\proves\vR\cumul\vT}
215\Rule{\Gamma\proves\vS_1\converts\vS_2\hg\Gamma;\vx\Hab\vS_1\proves\vT_1\cumul\vT_2}
216{\Gamma\proves\all{\vx}{\vS_1}\SC\vT_1\cumul\all{\vx}{\vS_2}{\vT_2}}
222\subsection{Inductive Families}
224\label{sect:inductivefams}
226Inductive families \cite{dybjer1994inductive} are a form of simultaneously
227defined collection of algebraic data types which can be parametrised over
228\remph{values} as well as types. An inductive family is declared
229in a similar style to a Haskell GADT declaration~\cite{pj2006gadts}
231follows, using the de Bruijn telescope notation, $\tx$, to indicate a
232sequence of zero or more $\vx$ (i.e., $\vx_1,\vx_2,\ldots,\vx_n$):
236\Data\hg\TC{T}\:(\tx\Hab\ttt)\Hab\vt\hg\Where\hg
237\DC{c}_1\Hab\vt\:\mid\:\ldots\:\mid\:\DC{c}_n\Hab\vt
241Constructors may take recursive arguments in the family
242$\TC{T}$. Furthermore these arguments may themselves be indexed by another type ---
243if such indices do not involve $\TC{T}$ then the constructor is
244\demph{strictly positive}, which ensures that recursive arguments of the
245constructor are structurally smaller than the value itself.
247For example, the \Idris{} data type \tTC{Nat} would be declared in \TT{} as follows:
250\Data\hg\Nat\Hab\Type\hg\Where\hg\Z\Hab\Nat\:\mid\:\suc\Hab\fbind{\vk}{\Nat}{\Nat}
253A data type may have zero or more parameters (which are invariant
254across a structure) and a number of indices, given by the type. For
255example, the \TT{} equivalent of \tTC{List} is parametrised over its element type:
259\Data\hg\List\:(\va\Hab\Type)\Hab\Type\hg\Where
261& \nil\Hab\List\:\va\\
262\mid & (\cons)\Hab\fbind{\vx}{\va}{\fbind{\vxs}{\List\:\va}{\List\:\va}}
268parametrised over values. Using this, we can declare the type of
269vectors (lists with length), where the empty list is statically known
270to have length zero, and the non empty list is statically known to
271have a non zero length. The \TT{} equivalent of \tTC{Vect} is parametrised over its element type,
272like $\List$, but \remph{indexed} over its length. Note also that the length
273index $\vk$ is given \remph{explicitly}.
277\Data\hg\Vect\:(\va\Hab\Type)\Hab\Nat\to\Type\hg\Where \\
279& \nil\Hab\Vect\:\va\:\Z\\
280\mid & (\cons)\Hab\fbind{\vk}{\Nat}{
281\fbind{\vx}{\va}{\fbind{\vxs}{\Vect\:\va\:\vk}{\Vect\:\va\:(\suc\:\vk)}}
287\subsection{Pattern matching definitions}
291\subsubsection{Syntax}
293A pattern matching definition for a function named $\FN{f}$ takes the following form,
294consisting of a type declaration followed by one or more pattern clauses:
299\pat{\tx_1}{\ttt_1}\SC\FN{f}\:\ttt_1\:=\:\vt_1\\
301\pat{\tx_n}{\ttt_n}\SC\FN{f}\:\ttt_n\:=\:\vt_n\\
305A pattern clause consists of a list of pattern variable bindings,
306and a left and right hand side, both of which
307are \TT{} expressions. Each side is type checked relative to the variable bindings,
308and the types of each side must be convertible. Additionally, the
309left hand side must take the form of $\FN{f}$ applied to a number of \TT{} expressions,
310and the number of arguments must be the same in each clause. The right hand
311sides may include applications of $\FN{f}$, i.e. pattern matching definitions may
312be recursive. Termination analysis is implemented separately. The validity of a pattern
313clause is defined by the following rule:
317\Gamma;\lam{\tx}{\tU}\proves\FN{f}\:\tts\Hab\vS\hg
318\Gamma;\lam{\tx}{\tU}\proves\ve\Hab\vT\hg
319\Gamma\proves\vS\converts\vT}
321\Gamma\proves\pat{\tx}{\tU}\SC\FN{f}\:\tts\:=\:\ve\:\RW{valid}
325A valid pattern matching definition effectively extends \TT{} with a new constant,
326with the given type (extending the initial typing rules given in Section \ref{sect:typerules})
327and reduction behaviour (extending the initial reduction rules given in Section
328\ref{sect:evaluation}).
330\subsubsection{Semantics}
332Matching on an expression proceeds by comparing the expression to
333each match clause in order, resulting in either:
336\item \demph{Success}, with pattern variables mapping to expressions
337\item \demph{Failure}, with matching continuing by proceeding to the next match clause
338\item Matching being \demph{blocked}, for example by attempting to match a variable
339against a constructor pattern. In this case, no reduction occurs, because instantiating
340the variable may provide enough information for the clause to match.
343% Pat(x args) => x (Pat' args)
347In order to implement pattern matching, we must separate the \remph{accessible} and
348\remph{inaccessible} patterns. A pattern is \demph{accessible} (that is, it is possible
349to match against it) if it is constructor headed, or a variable. Inaccessible patterns
350are converted to ``match anything'' patterns. We convert clauses to matchable pattern
351clauses with the $\MO{Clause}$ operation, given in Figure \ref{mkclause}.
352We extend the telescope notation to meta-operations: the notation $\vec{\MO{Pat}}$ lifts the
353$\MO{Pat}$ operation across a list of arguments.
358& \MO{Clause} & (\pat{\tx}{\tU}\SC\FN{f}\:\tts\:=\:\ve)
359 & \MoRet{\FN{f}\:(\vec{\MO{Pat}}\:\tts)\:=\:\ve}
363& \MO{Pat} & (\vx\:\tts) & \MoRet{\vx\:(\vec{\MO{Pat}}\:\tts)
364 \hg\mbox{(if $\MO{Con}\:\vx$ and $\MO{Arity}\:\vx = \MO{Length}\:\tts$)}} \\
365& \MO{Pat} & \vx & \MoRet{\vx} \hg\mbox(if $\vx$ is a pattern variable)\\
366& \MO{Pat} & \cdot & \MoRet{\_} \hg\mbox(in all other cases)\\
370{Building matchable pattern clauses}
374% Match (c args, c args') => Match' (args, args')
375% Match (c args, x) => Blocked
376% Match (x, t) => Success (x => t)
377% Match (_, t) => Success ()
379\newcommand{\Blocked}{\mathsf{Blocked}}
380\newcommand{\Success}{\mathsf{Success}}
381\newcommand{\Failure}{\mathsf{Failure}}
383Pattern matching is invoked by the evaluator on encountering a function with
384a pattern matching definition applied to some arguments. If successful, pattern
385matching returns a new expression, which can then be reduced further.
386Figure \ref{pmatch} gives the semantics of pattern matching a collection of
388$\tc$ against an expression $\ve$. $\MO{Match}$ attempts to match each clause in
389turn against $\ve$. If matching a clause returns $\Success$ or $\Blocked$, then
390matching terminates. If matching a clause returns $\Failure$, then matching proceeds
391with the next clause. The algorithm uses the following meta-operations:
394\item $\MO{Con}\:\vx$, which returns true if $\vx$ is a constructor name
395\item $\MO{Arity}\:\vx$, which, if $\vx$ is a constructor name, returns the number of arguments
397\item $\MO{Length}\:\tts$, which returns the length of the telescope $\tts$
404& \MO{MatchArg} & (\vx\:\tts) & (\vx\:\tts')
405 & \MoRet{\vec{\MO{MatchArg}}\:\tts\:\tts'\hg\mbox{(if $\MO{Con}\:\vx$)}}\\
406& \MO{MatchArg} & (\vx\:\tts) & \vx & \MoRet{\Blocked} \\
407& \MO{MatchArg} & \vx & \vt & \MoRet{\Success\:(\vx\mapsto\vt)} \\
408& \MO{MatchArg} & \_ & \vt & \MoRet{\Success\:()} \\
409& \MO{MatchArg} & \cdot & \cdot & \MoRet{\Failure}
413& \MO{MatchClause} & (\vf\:\tp = \ve) & (\vf\:\tts) &
416 \Success\:\ve[\tx/\tv]\hg\mbox{(if $\vec{\MO{MatchArg}}\:\tp\:\tts \mq \Success\:(\tx,\tv)$)}\\
417 \Blocked\hg\mbox{(if $\vec{\MO{MatchArg}}\:\tp\:\tts \mq \Blocked$)}\\
418 \Failure\hg\mbox{(if $\vec{\MO{MatchArg}}\:\tp\:\tts \mq \Failure$)}\\
421& \MO{MatchClause} & (\vf\:\tp = \ve) & \cdot & \MoRet{\Failure} \\
425& \MO{Match} & (\vc ; \tc) & \ve &
428 \Success\:\vx\hg\mbox{(if $\MO{MatchClause}\:\vc\:\ve \mq \Success\:\vx)$} \\
429 \Blocked\hg\mbox{(if $\MO{MatchClause}\:\vc\:\ve \mq \Blocked)$} \\
430 \MO{Match}\:\tc\:\ve\hg\mbox{(otherwise)}
433& \MO{Match} & \cdot & \ve & \MoRet{\Failure}
437{Pattern matching semantics}
440By convention, we write the application of a meta-operation $\MO{Op}$
441to a telescope $\tx$ as $\vec{\MO{Op}}\:\tx$.
442In practice, for efficiency, pattern matching is implemented by compiling the match clauses to
443a tree of case expressions~\cite{Augustsson1985}.
445\subsection{From \Idris{} to \TT{}}
447\TT{} is a very small language, consisting only of data declarations and pattern matching
448function definitions. There is no significant innovation in the design of \TT{}, and this
449is a deliberate choice --- it is a combination of small, well-understood components.
450The kernel of the \TT{} implementation, consisting of a type checker, evaluator and
451pattern match compiler, is less than 1000 lines of Haskell code. If we are confident
452in the correctness of the kernel of \TT{}, and any higher level language feature
453can be translated into \TT{}, we can be more confident of the correctness of the high
454level language implementation than if it were implemented directly.
456The process of elaborating a high level language into a core type theory like \TT{} is,
457however, less well understood, and presents several challenges depending on the
458features of the high level language.
459%Elaboration has been implemented in various different ways,
460%for example in Agda~\cite{norell2007thesis} and Epigram~\cite{McBride2004a}.
462\subsubsection{Example Elaboration}
464Consider the following \Idris{} function:
466\begin{SaveVerbatim}{vadd}
468vAdd : Num a => Vect a n -> Vect a n -> Vect a n
470vAdd (x :: xs) (y :: ys) = x + y :: vAdd xs ys
476This adds corresponding elements of vectors of the same length. The vectors can contain
477any numeric type, overloaded using the \texttt{Num} type class. In order to elaborate
478this to \TT{}, we must resolve the implicit arguments, and make the type class explicit.
480The first step is to make the implicit arguments explicit, using a placeholder
481to stand for the arguments we have not yet resolved. The type class argument is
482also treated as an implicit argument, to which we give the name \texttt{c}:
484\begin{SaveVerbatim}{vAddImp}
486vAdd : (a : _) -> (n : _) -> Num a -> Vect a n -> Vect a n -> Vect a n
487vAdd _ _ c (Nil _) (Nil _) = (Nil _)
488vAdd _ _ c ((::) _ _ x xs) ((::) _ _ y ys)
489 = (::) _ _ ((+) _ x y) (vAdd _ _ _ xs ys)
494Next, we resolve the implicit arguments. Each implicit argument can only take
495one value for this program to be type correct --- these are solved by a unification
498\begin{SaveVerbatim}{vAddImpSolve}
500vAdd : (a : Set) -> (n : Nat) -> Num a -> Vect a n -> Vect a n -> Vect a n
501vAdd a O c (Nil a) (Nil a) = Nil a
502vAdd a (S k) c ((::) a k x xs) ((::) a k y ys)
503 = (::) a k ((+) c x y) (vAdd a k c xs ys)
506\useverb{vAddImpSolve}
508Finally, to build the \TT{} definition, we need to find the type of each pattern variable
509and state it explicitly. This leads to the \TT{} definition in Figure \ref{ttvadd},
510switching to \TT{} notation from the ASCII \Idris{} syntax.
515\FN{vAdd} & \Hab(\va\Hab\Set)\to(\vn\Hab\Nat)\to\TC{Num}\:\va\to
516 \Vect\:\va\:\vn\to\Vect\:\va\:\vn\to\Vect\:\va\:\vn\\
519\begin{array}{lccccccc}
521\RW{var}\:\va\Hab\Set,\:\vc\Hab\TC{Num}\;\va\SC}\\
522\hg\FN{vAdd} & \va & \Z & \vc & (\DC{Nil}\;\va) & (\DC{Nil}\;\va) & \Ret{\DC{Nil}\;\va} \\
525\va\Hab\Set,\:\vk\Hab\Nat,\;\vc\Hab\TC{Num}\;\va,\\
526\vx\Hab\va,\;\vxs\Hab\Vect\;\va\;\vk,\;
527\vy\Hab\va,\;\vys\Hab\Vect\;\va\;\vk
531\hg\FN{vAdd} & \va & (\suc\;\vk) & \vc
532 & ((\DC{::})\;\va\;\vk\;\vx\;\vxs)
533 & ((\DC{::})\;\va\;\vk\;\vy\;\vys)
535 & & \MRet{5}{((\DC{::})\;\va\;\vk\;((+)\;\vc\;\vx\;\vy)\; (\FN{vAdd}\;\va\;\vk\;\vc\;\vxs\;\vys))}
539{Pairwise addition of vectors in \TT{}}
542\subsubsection{An observation}
544\Idris{} programs may contain several high level constructs not present in \TT{}, such
545as implicit arguments, type classes, \texttt{where} clauses, pattern matching \texttt{let}
546and \texttt{case} constructs. We would like the high level language to be as expressive
547as possible, while remaining possible to translate to \TT{}.
549Before considering how to achieve this, we make an observation about the distinction between
550programming and theorem proving with dependent types, and appropriate mechanisms for
551constructing programs and theorems:
554\item \remph{Pattern matching} is a convenient abstraction for humans to write programs,
555in that it allows a programmer to express exactly the computational behaviour of a function.
556\item \remph{Tactics}, such as those used in the Coq theorem prover~\cite{Bertot2004},
557are a convenient abstraction for building proofs and programs by \remph{refinement}.
560The idea behind the \Idris{} elaborator, therefore, is to use the high level program
561to direct \demph{tactics} to build \TT{} programs by refinement. We implement the
562elaborator as an Embedded Domain Specific Language (EDSL) in Haskell.
564of this paper, we decribe the EDSL, and demonstrate how it can be used to implement
565all 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