1\section{The Core Type Theory}
3\label{sect:typechecking}
5High-level \Idris{} programs, as described in Section \ref{sect:hll}, are
6\remph{elaborated} to a small core language, \TT{}, then type checked.
7\TT{} is a dependently-typed $\lambda$-calculus with inductive families
8and pattern matching definitions similar to UTT~\cite{luo1994}, and building
9on an earlier implementation, \Ivor{}~\cite{Brady2006b}.
11core language is kept as small as is reasonably possible, which has several advantages: it is
12easy to type check, since type checking dependent type theory is well understood
13~\cite{loh2010tutorial}; and it is easy to transform, optimise and compile. Keeping
14the core language small increases confidence that these important components of
15the language are correct. In this section, we describe \TT{} and
18\subsection{\TT{} syntax}
20The syntax of \TT{} expressions is given in Figure \ref{ttsyn}. This defines:
23\item \demph{Terms}, $\vt$, which can be variables, bindings, applications or constants.
24\item \demph{Bindings}, $\vb$, which can be lambda abstractions, let bindings, or function spaces.
25\item \demph{Constants}, $\vc$, which can be integer or string literals, or $\Type_i$, the
26type of types, and may be extended with other primitives.
29The function space $\all{\vx}{\vS}\SC\vT$ may also be written as $(\vx\Hab\vS)\to\vT$,
30or $\vS\to\vT$ if $\vx$ is not free in $\vT$, to make the notation more consistent with
31the high-level language. Universe levels on types ($\Type_i$) may be left implicit and
32inferred by the machine~\cite{pollack1990implicit}.
35\begin{array}{rll@{\hg}rll}
36\mbox{Terms,}\;\vt ::= & \vc & (\mbox{constant}) &
37\;\mbox{Binders,}\;\vb ::= & \lam{\vx}{\vt} & (\mbox{abstraction}) \\
39 \mid & \vx & (\mbox{variable}) &
40 \mid & \LET\;\vx\defq\vt\Hab\vt & (\mbox{let binding}) \\
42 \mid & \vb\SC\;\vt & (\mbox{binding}) &
43 \mid & \all{\vx}{\vt} & (\mbox{function space}) \\
45 \mid & \vt\;\vt & (\mbox{application}) & \\
46 \mid & \TC{T} & (\mbox{type constructor}) & \\
47 \mid & \TC{D} & (\mbox{data constructor}) &
48% \mid & \pat{\vx}{\vt} & (\mbox{pattern variable}) \\
50% \mid & \pty{\vx}{\vt} & (\mbox{pattern type}) \\
52\mbox{Constants,}\;\vc ::= & \Type_i & (\mbox{type universes}) \\
53 \mid & \vi & (\mbox{integer literal}) \\
54 \mid & \VV{str} & (\mbox{string literal}) \\
57{\TT{} expression syntax}
60A \TT{} program is a collection of \demph{inductive family} definitions (Section
61\ref{sect:inductivefams}) and \demph{pattern matching} function definitions (Section
62\ref{sect:patdefs}), as well as primitive operators on constants.
63Before defining these, let us define the semantics of \TT{}
66\subsection{\TT{} semantics}
68The static and dynamic semantics of \TT{} are defined mutually, since
69evaluation relies on a well-typed term, and type checking relies on
70evaluation. Everything is defined relative
71to a context, $\Gamma$. The empty context
72is valid, as is a context extended with a $\lambda$, $\forall$ or
76\Axiom{\proves\RW{valid}}
78\Rule{\Gamma\proves\vS\Hab\Type_i}
79{\Gamma;\lam{\vx}{\vS}\proves\RW{valid}}
81\Rule{\Gamma\proves\vS\Hab\Type_i}
82{\Gamma;\all{\vx}{\vS}\proves\RW{valid}}
84\Rule{\Gamma\proves\vS\Hab\Type_i\hg\Gamma\proves\vs\Hab\vS}
85{\Gamma;\LET\;\vx\;\defq\;\vs\Hab\vS\proves\RW{valid}}
89We record the binding form in the context, as well as the type,
90because type checking relies on evaluation. In particular, $\LET$ bound
93\subsubsection{Evaluation}
95\label{sect:evaluation}
97There are two distinct phases in which \TT{} evaluation occurs, namely
98\demph{compile-time} and \demph{run-time}. Compile-time evaluation is primarily
99to support type-checking, in which equivalence of two terms (or types) is
100determined by comparing their normal forms. It is important that terms are
101strongly normalising at compile-time, so any pattern matching definition which
102is not guaranteed to be total does not reduce. In this section we discuss
103compile-time evaluation; run-time evaluation differs in that there is no
104reduction under binders, types and duplicated values have been
105erased~\cite{Brady2003}, and non-normalising definitions may reduce.
107Compile-time evaluation of \TT{} is defined by contraction schemes, given in
108Figure \ref{ttcontract}. \demph{Contraction}, relative to a context $\Gamma$,
109is given by one of the following schemes:
112\item $\beta$-contraction, which substitutes a value applied to a $\lambda$-binding for
114%We define $\beta$-contraction simply by replacing the $\lambda$-binding
115%with a $\LET$ binding.
116\item $\delta$-contraction, which replaces a $\LET$ bound variable with its value.
120The following contextual closure rule reduces a $\LET$ binding by creating
121a $\delta$-reducible expression:
124\Rule{\Gamma;\LET\;\vx\defq\vs\Hab\vS\proves\vt\leadsto\vu}
125{\Gamma\proves\LET\;\vx\defq\vs\Hab\vS\SC\vt\leadsto\vu}
128\demph{Reduction} ($\reduces$) is the structural closure of contraction, and evaluation
129is ($\reducesto$) is the transitive closure of reduction. \demph{Conversion} ($\converts$)
130is the smallest equivalence relation closed under reduction. If $\Gamma\proves\vx\converts\vy$
131then $\vy$ can be obtained from $\vx$ by a finite, possibly empty, sequence of
132contractions and reversed contractions. Terms which are convertible are also said to
133be definitionally equal.
134The evaluator can also be extended by defining pattern matching functions, which
135will be described in more detail in Section \ref{sect:patdefs}. In principle, pattern
136matching functions can be understood as extending the core language with high-level
141\beta\mathrm{-contraction} &
143\Gamma\proves(\lam{\vx}{\vS}\SC\vt)\;\vs\leadsto
145%\LET\;\vx\defq\vs\Hab\vS\SC\vt
147\delta\mathrm{-contraction} &
149\Gamma;\LET\;\vx\defq\vs\Hab\vS;\Gamma'
155{\TT{} contraction schemes}
160\subsubsection{Typing rules}
162\label{sect:typerules}
164The type inference rules for \TT{} expressions are given in Figure
165\ref{typerules}. These rules use the \demph{cumulativity} relation, defined in
166Figure \ref{cumul}. The type of types, $\Type_i$ is parameterised by a universe
167level, to prevent Girard's paradox~\cite{coquand1986analysis}. There is an
168infinite hierarchy of predicative universes. Cumulativity allows programs at
169lower universe levels to inhabit higher universe levels. In practice, universe levels
170can be left implicit (and will be left implicit in the rest of this paper) ---
171the type checker generates a graph of constraints between universe levels (such
172as that produced by the $\mathsf{Forall}$ typing rule) and checks that there
173are no cycles. This happens as the last stage of type checking, waiting until
174we have all uses of a family to establish how many levels are needed in the
176Otherwise, the typing rules are standard and type inference can
177be implemented in the usual way~\cite{loh2010tutorial}.
179\FFIG{\begin{array}{c}
181\Rule{\Gamma\proves\RW{valid}}
182{\Gamma\vdash\Type_n\Hab\Type_{n+1}}
185\Rule{\Gamma\proves\RW{valid}}
186{\Gamma\vdash\vi\Hab\TC{Int}}
189\Rule{\Gamma\proves\RW{valid}}
190{\Gamma\vdash\VV{str}\Hab\TC{String}}
193\Rule{\Gamma\proves\RW{valid}}
194{\Gamma\vdash\TC{Int}\Hab\Type_0}
197\Rule{\Gamma\proves\RW{valid}}
198{\Gamma\vdash\TC{String}\Hab\Type_0}
201%\Rule{(\pat{\vx}{\vS})\in\Gamma}
202%{\Gamma\vdash\vx\Hab\vS}
205%\Rule{(\pty{\vx}{\vS})\in\Gamma}
206%{\Gamma\vdash\vx\Hab\vS}
209\Rule{(\lam{\vx}{\vS})\in\Gamma}
210{\Gamma\vdash\vx\Hab\vS}
213\Rule{(\all{\vx}{\vS})\in\Gamma}
214{\Gamma\vdash\vx\Hab\vS}
217\Rule{(\LET\;\vx\defq\vs\Hab\vS)\in\Gamma}
218{\Gamma\vdash\vx\Hab\vS}
221\Rule{\Gamma\vdash\vf\Hab\fbind{\vx}{\vS}{\vT}\hg\Gamma\vdash\vs\Hab\vS}
222{\Gamma\vdash\vf\;\vs\Hab\vT[\vs/\vx]} % \LET\;\vx\Hab\vS\;\defq\;\vs\;\IN\;\vT}
225\Rule{\Gamma;\lam{\vx}{\vS}\vdash\ve\Hab\vT\hg\Gamma\proves\fbind{\vx}{\vS}{\vT}\Hab\Type_n}
226{\Gamma\vdash\lam{\vx}{\vS}.\ve\Hab\fbind{\vx}{\vS}{\vT}}
229\Rule{\Gamma;\all{\vx}{\vS}\vdash\vT\Hab\Type_m\hg\Gamma\vdash\vS\Hab\Type_n}
230{\Gamma\vdash\fbind{\vx}{\vS}{\vT}\Hab\Type_p}
231\;(\exists\vp.\vm\le\vp,\;\vn\le\vp)
234\Rule{\begin{array}{c}\Gamma\proves\ve_1\Hab\vS\hg
235 \Gamma;\LET\;\vx\defq\ve_1\Hab\vS\proves\ve_2\Hab\vT\\
236 \Gamma\proves\vS\Hab\Type_n\hg
237 \Gamma;\LET\;\vx\defq\ve_1\Hab\vS\proves\vT\Hab\Type_n\end{array}
239{\Gamma\vdash\LET\;\vx\defq\ve_1\Hab\vS\SC\;\ve_2\Hab
241%\Let\;\vx\Hab\vS\defq\ve_1\;\IN\;\vT}
245\Rule{\Gamma\proves\vx\Hab\vA\hg\Gamma\proves\vA'\Hab\Type_n\hg
246 \Gamma\proves\vA\cumul\vA'}
247 {\Gamma\proves\vx\Hab\vA'}
250{Typing rules for \TT{}}
255\Rule{\Gamma\proves\vS\converts\vT}
256{\Gamma\proves\vS\cumul\vT}
258\Axiom{\Gamma\proves\Type_n\cumul\Type_{n+1}}
260\Rule{\Gamma\proves\vR\cumul\vS\hg\Gamma\proves\vS\cumul\vT}
261{\Gamma\proves\vR\cumul\vT}
263\Rule{\Gamma\proves\vS_1\converts\vS_2\hg\Gamma;\vx\Hab\vS_1\proves\vT_1\cumul\vT_2}
264{\Gamma\proves\all{\vx}{\vS_1}\SC\vT_1\cumul\all{\vx}{\vS_2}{\vT_2}}
271\subsection{Inductive Families}
273\label{sect:inductivefams}
275Inductive families \cite{dybjer1994inductive} are a form of simultaneously
276defined collection of algebraic data types which can be parameterised over
277\remph{values} as well as types. An inductive family is declared
278in a similar style to a Haskell GADT declaration~\cite{pj2006gadts}
284\Data\hg\TC{T}\Hab\vt\hg\Where\hg
285\DC{D}_1\Hab\vt\;\mid\;\ldots\;\mid\;\DC{D}_n\Hab\vt
289A constructor $\TC{D}$ of a family $\TC{T}$ must return a value in the family
291It may take recursive arguments in the family $\TC{T}$ which may be
293Using vector notation, $\tx$, to indicate a
294sequence of zero or more $\vx$ (i.e., $\vx_1,\vx_2,\ldots,\vx_n$),
295recursive arguments have types of the form
298\all{\vx_1}{\vS_1}\SC\ldots\all{\vx_n}{\vS_n}\SC\TC{T}\:\ty
301where $\TC{T}$ does not occur in any of the $\tS$ or the $\ty$
302This restriction is known as
303\demph{strict positivity} and ensures that recursive arguments of the
304constructor are structurally smaller than the value itself.
306practice, this restriction can be relaxed when defining a family, but definitions
307using families which do not satisfy strict positivity will not pass totality
310For example, the \Idris{} data type \tTC{Nat} would be declared in \TT{} as follows:
313\Data\hg\Nat\Hab\Type\hg\Where\hg\Z\Hab\Nat\;\mid\;\suc\Hab\fbind{\vk}{\Nat}{\Nat}
316A data type may have zero or more parameters (which are invariant
317across a structure) and a number of indices, given by the type. For example,
318the \TT{} equivalent of \tTC{List} is parameterised over its element type:
322\Data\hg\List\Hab(\va\Hab\Type)\to\Type\hg\Where\\
325& \nil\Hab\List\;\va\\
326\mid & (\cons)\Hab\fbind{\vx}{\va}{\fbind{\vxs}{\List\;\va}{\List\;\va}}
332parameterised or indexed over values. Using this, we can declare the type of
333vectors (lists with length), where the empty list is statically known
334to have length zero, and the non empty list is statically known to
335have a non zero length. The \TT{} equivalent of \tTC{Vect} is parameterised over its element type,
336like $\List$, but \remph{indexed} over its length. Note also that the length
337index $\vk$ is given \remph{explicitly}.
341\Data\hg\Vect\Hab\Nat\to(\va\Hab\Type)\to\Type\hg\Where \\
343& \nil\Hab\Vect\;\Z\;\va\\
344\mid & (\cons)\Hab\fbind{\vk}{\Nat}{
345\fbind{\vx}{\va}{\fbind{\vxs}{\Vect\;\vk\;\va}{\Vect\;(\suc\;\vk)\;\va}}
351\subsection{Pattern matching definitions}
355%\subsubsection{Syntax}
358A pattern matching definition for a function named $\FN{f}$ takes the following form,
359consisting of a type declaration followed by one or more pattern clauses:
364\pat{\tx_1}{\ttt_1}\SC\FN{f}\;\ttt_1\;=\;\vt_1\\
366\pat{\tx_n}{\ttt_n}\SC\FN{f}\;\ttt_n\;=\;\vt_n\\
370A pattern clause consists of a list of pattern variable bindings, introduced by
372and a left and right hand side, both of which
373are \TT{} expressions. Each side is type checked relative to the variable bindings,
374and the types of each side must be convertible. Additionally, the
375left hand side must take the form of $\FN{f}$ applied to a number of \TT{} expressions,
376and the number of arguments must be the same in each clause. The right hand
377sides may include applications of $\FN{f}$, i.e. pattern matching definitions may
378be recursive. The validity of a pattern
379clause is defined by the following rule:
383\Gamma;\lam{\tx}{\tU}\proves\FN{f}\;\tts\Hab\vS\hg
384\Gamma;\lam{\tx}{\tU}\proves\ve\Hab\vT\hg
385\Gamma\proves\vS\converts\vT}
387\Gamma\proves\pat{\tx}{\tU}\SC\FN{f}\;\tts\;=\;\ve\;\RW{valid}
391Patterns are separated into the accessible patterns (variables and constructor
392forms which may be inspected) and inaccessible patterns, following
393Agda~\cite{norell2007thesis} then implemented by compilation into case
394trees~\cite{Augustsson1985}. Non-terminating definitions are permitted, but do
395not reduce at compile-time, which means in particular that they cannot be used
397Termination analysis is implemented separately.
399A valid pattern matching definition effectively extends \TT{} with a new
400constant, with the given type (extending the initial typing rules given in
401Section \ref{sect:typerules}) and reduction behaviour (extending the initial
402reduction rules given in Section \ref{sect:evaluation}).
405% \subsubsection{Semantics}
407% Matching on an expression proceeds by comparing the expression to
408% each match clause in order, resulting in either:
411% \item \demph{Success}, with pattern variables mapping to expressions
412% \item \demph{Failure}, with matching continuing by proceeding to the next match clause
413% \item Matching being \demph{blocked}, for example by attempting to match a variable
414% against a constructor pattern. In this case, no reduction occurs, because instantiating
415% the variable may provide enough information for the clause to match.
418% % Pat(x args) => x (Pat' args)
422% In order to implement pattern matching, we must separate the \remph{accessible} and
423% \remph{inaccessible} patterns. A pattern is \demph{accessible} (that is, it is possible
424% to match against it) if it is constructor headed, or a variable. Inaccessible patterns
425% are converted to ``match anything'' patterns. Clauses are converted to matchable pattern
426% clauses with the $\MO{Clause}$ operation, given in Figure \ref{mkclause}.
427% We extend the vector notation to meta-operations: the notation $\vec{\MO{Pat}}$ lifts the
428% $\MO{Pat}$ operation across a list of arguments.
433% & \MO{Clause} & (\pat{\tx}{\tU}\SC\FN{f}\;\tts\;=\;\ve)
434% & \MoRet{\FN{f}\;(\vec{\MO{Pat}}\;\tts)\;=\;\ve}
438% & \MO{Pat} & (\vx\;\tts) & \MoRet{\vx\;(\vec{\MO{Pat}}\;\tts)
439% \hg\mbox{(if $\MO{Con}\;\vx$ and $\MO{Arity}\;\vx = \MO{Length}\;\tts$)}} \\
440% & \MO{Pat} & \vx & \MoRet{\vx} \hg\mbox(if $\vx$ is a pattern variable)\\
441% & \MO{Pat} & \cdot & \MoRet{\_} \hg\mbox(in all other cases)\\
445% {Building matchable pattern clauses}
449% % Match (c args, c args') => Match' (args, args')
450% % Match (c args, x) => Blocked
451% % Match (x, t) => Success (x => t)
452% % Match (_, t) => Success ()
454% \newcommand{\Blocked}{\mathsf{Blocked}}
455% \newcommand{\Success}{\mathsf{Success}}
456% \newcommand{\Failure}{\mathsf{Failure}}
458% Pattern matching is invoked by the evaluator on encountering a function with
459% a pattern matching definition applied to some arguments. If successful, pattern
460% matching returns a new expression, which can then be reduced further.
461% Figure \ref{pmatch} gives the semantics of pattern matching a collection of
463% $\tc$ against an expression $\ve$. $\MO{Match}$ attempts to match each clause in
464% turn against $\ve$. If matching a clause returns $\Success$ or $\Blocked$, then
465% matching terminates. If matching a clause returns $\Failure$, then matching proceeds
466% with the next clause. The algorithm uses the following meta-operations:
469% \item $\MO{Con}\;\vx$, which returns true if $\vx$ is a constructor name
470% \item $\MO{Arity}\;\vx$, which, if $\vx$ is a constructor name, returns the number of arguments
472% \item $\MO{Length}\;\tts$, which returns the length of the vector $\tts$
479% & \MO{MatchArg} & (\vx\;\tts) & (\vx\;\tts')
480% & \MoRet{\vec{\MO{MatchArg}}\;\tts\;\tts'\hg\mbox{(if $\MO{Con}\;\vx$)}}\\
481% & \MO{MatchArg} & (\vx\;\tts) & \vx & \MoRet{\Blocked} \\
482% & \MO{MatchArg} & \vx & \vt & \MoRet{\Success\;(\vx\mapsto\vt)} \\
483% & \MO{MatchArg} & \_ & \vt & \MoRet{\Success\;()} \\
484% & \MO{MatchArg} & \cdot & \cdot & \MoRet{\Failure}
488% & \MO{MatchClause} & (\vf\;\tp = \ve) & (\vf\;\tts) &
491% \Success\;\ve[\tx/\tv]\hg\mbox{(if $\vec{\MO{MatchArg}}\;\tp\;\tts \mq \Success\;(\tx,\tv)$)}\\
492% \Blocked\;\;\;\hg\hg\mbox{(if $\vec{\MO{MatchArg}}\;\tp\;\tts \mq \Blocked$)}\\
493% \Failure\;\;\;\;\;\hg\hg\mbox{(if $\vec{\MO{MatchArg}}\;\tp\;\tts \mq \Failure$)}\\
496% & \MO{MatchClause} & (\vf\;\tp = \ve) & \cdot & \MoRet{\Failure} \\
500% & \MO{Match} & (\vc ; \tc) & \ve &
503% \Success\;\vx\;\;\hg\mbox{(if $\MO{MatchClause}\;\vc\;\ve \mq \Success\;\vx)$} \\
504% \Blocked\hg\;\;\;\;\mbox{(if $\MO{MatchClause}\;\vc\;\ve \mq \Blocked)$} \\
505% \MO{Match}\;\tc\;\ve\hg\mbox{(otherwise)}
508% & \MO{Match} & \cdot & \ve & \MoRet{\Failure}
512% {Pattern matching semantics}
515% By convention, we write the application of a meta-operation $\MO{Op}$
516% across a vector $\tx$ as $\vec{\MO{Op}}\;\tx$.
517% In practice, for efficiency, pattern matching is implemented by compiling the match clauses to
518% a tree of case expressions~\cite{Augustsson1985}.
520\subsection{Metatheory}
524\mbox{\textbf{Church-Rosser}} &
526\mbox{If}\hg\Gamma\proves\vs\converts\vt \\
527\mbox{then there is a common reduct $\vr$ such that}\;\\
528\Gamma\proves\vs\reducesto\vr\hg\Gamma\proves\vt\reducesto\vr
532\mbox{\textbf{Subject Reduction}} &
534\mbox{If} & \Gamma\proves\vs\Hab\vS\hg\Gamma\proves\vs\reduces\vt\\
535\mbox{then}& \Gamma\proves\vt\Hab\vS
541\mbox{If} & \Gamma_0,\LET\;\vx\defq\vs\Hab\vS,\Gamma_1\proves\vt\Hab\vT\\
542\mbox{then} & \Gamma_0, \Gamma_1[\vs/\vx]\proves\vt[\vs/\vx]\Hab\vT[\vs/\vx]
546\mbox{\textbf{Strengthening}} &
548\mbox{If} & \Gamma_0,\mathcal{B}(\vx, \vT),\Gamma_1\proves\vs\Hab\vS
549\hg\vx\not\in\Gamma_1,\vs,\vS\\
550\mbox{then} & \Gamma_0,\Gamma_1\proves\vs\Hab\vS\\
551(\mbox{where} & \mathcal{B}(\vx, \vT) \proves \vx\Hab\vT)
555\mbox{\textbf{Strong normalisation}} &
557\mbox{If} & \Gamma\proves\vt\Hab\vT\\
558\mbox{then} & \vt\:\mbox{is strongly normalising}\\
563{Metatheoretic properties of \TT{}}
566We conjecture that \TT{} respects the usual metatheoretic properties,
568Figure \ref{metatheory}. Specifically: the \demph{Church-Rosser} property
569(i.e. that distinct reduction sequences lead to the same normal form);
570\demph{subject reduction} (i.e. that computation preserves type); the
571\demph{cut} property (i.e. that $\RW{let}$-bound terms may be substituted into
572their scope); and \demph{strengthening} (i.e. that removing unused definitions
573from scope does not affect type checking).
574\demph{Strong normalisation} holds at compile-time because pattern matching
575definitions which cannot be shown to be terminating do not have compile-time
578%One property which is noticeably absent is \demph{strong normalisation}.
579%Although desirable to preserve termination and decidability of type checking,
580%we allow diverging terms for pragmatic reasons as \Idris{} is primarily a
581%programming language rather than a theorem prover. Nevertheless, we do
582%\emph{check} for totality in order to be sure which terms are safe to
583%evaluate at compile time.
585\subsection{Totality checking}
587In order to ensure termination of type checking we must distinguish terms for
588which evaluation definitely terminates, and those which may diverge. \TT{}
589takes a simple but pragmatic and effective approach to termination checking:
590any functions which do not satisfy a syntactic constraint on recursive calls
591are marked as \emph{partial}. Additionally, any function which calls a partial
592function or uses a data type which is not strictly positive is also marked as
593partial. We use the size change principle~\cite{Lee2001} to determine whether
594(possibly mutually defined) recursive functions are guaranteed to
595terminate. Higher order function arguments are assumed to be total, though
596if a higher order function is called with a partial function as an argument,
597the calling function will be marked partial.
598\TT{} also marks functions which do not cover
599all possible inputs as partial. This totality checking is independent of the
600rest of the type theory, and can be extended.
602This approach, separating the termination requirement from the type theory,
603means that an \Idris{} programmer makes the decision about the importance of
604totality for each function rather than having the totality requirement imposed
607\subsection{From \Idris{} to \TT{}}
609\TT{} is a very small language, consisting only of data declarations and pattern matching
610function definitions. There is no significant innovation in the design of \TT{}, and this
611is a deliberate choice --- it is a combination of small, well-understood components.
612The kernel of the \TT{} implementation, consisting of a type checker, evaluator and
613pattern match compiler, is less than 1000 lines of Haskell code. If we are confident
614in the correctness of the kernel of \TT{}, and any higher level language feature
615can be translated into \TT{}, we can be more confident of the correctness of
616the high-level language implementation than if it were implemented directly.
618The process of elaborating a high-level language into a core type theory like \TT{} is,
619however, less well understood, and presents several challenges depending on the
620features of the high-level language.
621%Elaboration has been implemented in various different ways,
622%for example in Agda~\cite{norell2007thesis} and Epigram~\cite{McBride2004a}.
624\subsubsection{Example Elaboration}
626Recall the following \Idris{} function:
632this to \TT{}, we must resolve the implicit arguments, and make the type class explicit.
633The first step is to make the implicit arguments explicit, using a placeholder
634to stand for the arguments we have not yet resolved. The type class argument is
635also treated as an implicit argument, to which we give the name \texttt{c}:
637\begin{SaveVerbatim}{vAddImp}
639vAdd : (a : _) -> (n : _) ->
640 Num a -> Vect n a -> Vect n a -> Vect n a
641vAdd _ _ c (Nil _) (Nil _) = (Nil _)
642vAdd _ _ c ((::) _ _ x xs) ((::) _ _ y ys)
643 = (::) _ _ ((+) _ x y) (vAdd _ _ _ xs ys)
648Next, we resolve the implicit arguments. Each implicit argument can only take
649one value for this program to be type correct --- these are solved by a unification
652\begin{SaveVerbatim}{vAddImpSolve}
654vAdd : (a : Type) -> (n : Nat) ->
655 Num a -> Vect n a -> Vect n a -> Vect n a
656vAdd a O c (Nil a) (Nil a) = Nil a
657vAdd a (S k) c ((::) a k x xs) ((::) a k y ys)
658 = (::) a k ((+) c x y) (vAdd a k c xs ys)
661\useverb{vAddImpSolve}
663Finally, to build the \TT{} definition, we need to find the type of each
664pattern variable and state it explicitly. This leads to the following
665\TT{} definition, switching to \TT{} notation from the ASCII \Idris{}
670\FN{vAdd} \Hab(\va\Hab\Type)\to(\vn\Hab\Nat)\to\TC{Num}\;\va\to
671 \Vect\;\vn\;\va\to\Vect\;\vn\;\va\to\Vect\;\vn\;\va\\
672\RW{var}\;\va\Hab\Type,\;\vc\Hab\TC{Num}\;\va\SC\\
673\hg\FN{vAdd} \; \va \; \Z \; \vc \; (\DC{Nil}\;\va) \; (\DC{Nil}\;\va) \;
676\va\Hab\Type,\;\vk\Hab\Nat,\;\vc\Hab\TC{Num}\;\va,\\
677\vx\Hab\va,\;\vxs\Hab\Vect\;\vk\;\va,\;
678\vy\Hab\va,\;\vys\Hab\Vect\;\vk\;\va
681\FN{vAdd} \; \va \; (\suc\;\vk) \; \vc
682 \; ((\DC{::})\;\va\;\vk\;\vx\;\vxs)
683 \; ((\DC{::})\;\va\;\vk\;\vy\;\vys)
685 \hg\hg\cq\:((\DC{::})\;\va\;\vk\;((+)\;\vc\;\vx\;\vy)\; (\FN{vAdd}\;\va\;\vk\;\vc\;\vxs\;\vys))
690\subsubsection{An Observation: Programming vs Theorem Proving}
692\Idris{} programs may contain several high-level constructs not present in \TT{}, such
693as implicit arguments, type classes, \texttt{where} clauses, pattern matching \texttt{let}
694and \texttt{case} constructs. We would like the high-level language to be as expressive
695as possible, while remaining possible to translate to \TT{}.
697Before considering how to achieve this, we make an observation about the distinction between
698programming and theorem proving with dependent types, and appropriate mechanisms for
699constructing programs and theorems:
702\item \remph{Pattern matching} is a convenient abstraction for humans to write
703programs, in that it allows a programmer to express exactly the computational
704behaviour of a function.
705\item \remph{Tactics}, such as those used in the Coq theorem
706prover~\cite{Bertot2004}, are a convenient abstraction for building proofs and
707programs by \remph{refinement}.
710The idea behind the \Idris{} elaborator, therefore, is to use the high-level
711program to direct \demph{tactics} to build \TT{} programs by refinement. The
712elaborator is implemented as a Haskell monad capturing proof state, with a
713collection of tactics for updating and refining the proof state. The remainder
714of this paper describes this elaborator and demonstrates how it is used to
715implement 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