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 & \pat{\vx}{\vt} & (\mbox{pattern variable}) \\
48% \mid & \pty{\vx}{\vt} & (\mbox{pattern type}) \\
50\mbox{Constants,}\;\vc ::= & \Type_i & (\mbox{type universes}) \\
51 \mid & \vi & (\mbox{integer literal}) \\
52 \mid & \VV{str} & (\mbox{string literal}) \\
55{\TT{} expression syntax}
58A \TT{} program is a collection of \demph{inductive family} definitions (Section
59\ref{sect:inductivefams}) and \demph{pattern matching} function definitions (Section
60\ref{sect:patdefs}), as well as primitive operators on constants.
61Before defining these, let us define the semantics of \TT{}
64\subsection{\TT{} semantics}
66The static and dynamic semantics of \TT{} are defined mutually, since
67evaluation relies on a well-typed term, and type checking relies on
68evaluation. Everything is defined relative
69to a context, $\Gamma$. The empty context
70is valid, as is a context extended with a $\lambda$, $\forall$ or
74\Axiom{\proves\RW{valid}}
76\Rule{\Gamma\proves\vS\Hab\Type_i}
77{\Gamma;\lam{\vx}{\vS}\proves\RW{valid}}
79\Rule{\Gamma\proves\vS\Hab\Type_i}
80{\Gamma;\all{\vx}{\vS}\proves\RW{valid}}
82\Rule{\Gamma\proves\vS\Hab\Type_i\hg\Gamma\proves\vs\Hab\vS}
83{\Gamma;\LET\;\vx\;\defq\;\vs\Hab\vS\proves\RW{valid}}
86\subsubsection{Evaluation}
88\label{sect:evaluation}
90Evaluation of \TT{} is defined by contraction schemes, given in Figure
91\ref{ttcontract}. \demph{Contraction}, relative to a context $\Gamma$, is given
92by one of the following schemes:
95\item $\beta$-contraction, which substitutes a value applied to a $\lambda$-binding for
97%We define $\beta$-contraction simply by replacing the $\lambda$-binding
98%with a $\LET$ binding.
99\item $\delta$-contraction, which replaces a $\LET$ bound variable with its value.
103The following contextual closure rule reduces a $\LET$ binding by creating
104a $\delta$-reducible expression:
107\Rule{\Gamma;\LET\;\vx\defq\vs\Hab\vS\proves\vt\leadsto\vu}
108{\Gamma\proves\LET\;\vx\defq\vs\Hab\vS\SC\vt\leadsto\vu}
111\demph{Reduction} ($\reduces$) is the structural closure of contraction, and evaluation
112is ($\reducesto$) is the transitive closure of reduction. \demph{Conversion} ($\converts$)
113is the smallest equivalence relation closed under reduction. If $\Gamma\proves\vx\converts\vy$
114then $\vy$ can be obtained from $\vx$ by a finite, possibly empty, sequence of
115contractions and reversed contractions. Terms which are convertible are also said to
116be definitionally equal.
117The evaluator can also be extended by defining pattern matching functions, which
118will be described in more detail in Section \ref{sect:patdefs}. In principle, pattern
119matching functions can be understood as extending the core language with high level
124\beta\mathrm{-contraction} &
126\Gamma\proves(\lam{\vx}{\vS}\SC\vt)\;\vs\leadsto
128%\LET\;\vx\defq\vs\Hab\vS\SC\vt
130\delta\mathrm{-contraction} &
132\Gamma;\LET\;\vx\defq\vs\Hab\vS;\Gamma'
138{\TT{} contraction schemes}
143\subsubsection{Typing rules}
145\label{sect:typerules}
147The type inference rules for \TT{} expressions are given in Figure
148\ref{typerules}. These rules use the \demph{cumulativity} relation, defined in
149Figure \ref{cumul}. The type of types, $\Type_i$ is parameterised by a universe
150level, to prevent Girard's paradox~\cite{coquand1986analysis}. There is an
151infinite hierarchy of predicative universes. Cumulativity allows programs at
152lower universe levels to inhabit higher universe levels. In practice, universe levels
153can be left implicit (and will be left implicit in the rest of this paper) ---
154the type checker generates a graph of constraints between universe levels (such
155as that produced by the $\mathsf{Forall}$ typing rule) and checks that there
156are no cycles. Otherwise, the typing rules are standard and type inference can
157be implemented in the usual way~\cite{loh2010tutorial}.
159\FFIG{\begin{array}{c}
161\Rule{\Gamma\proves\RW{valid}}
162{\Gamma\vdash\Type_n\Hab\Type_{n+1}}
165\Rule{\Gamma\proves\RW{valid}}
166{\Gamma\vdash\vi\Hab\TC{Int}}
169\Rule{\Gamma\proves\RW{valid}}
170{\Gamma\vdash\VV{str}\Hab\TC{String}}
173\Rule{\Gamma\proves\RW{valid}}
174{\Gamma\vdash\TC{Int}\Hab\Type_0}
177\Rule{\Gamma\proves\RW{valid}}
178{\Gamma\vdash\TC{String}\Hab\Type_0}
181%\Rule{(\pat{\vx}{\vS})\in\Gamma}
182%{\Gamma\vdash\vx\Hab\vS}
185%\Rule{(\pty{\vx}{\vS})\in\Gamma}
186%{\Gamma\vdash\vx\Hab\vS}
189\Rule{(\lam{\vx}{\vS})\in\Gamma}
190{\Gamma\vdash\vx\Hab\vS}
193\Rule{(\all{\vx}{\vS})\in\Gamma}
194{\Gamma\vdash\vx\Hab\vS}
197\Rule{(\LET\;\vx\defq\vs\Hab\vS)\in\Gamma}
198{\Gamma\vdash\vx\Hab\vS}
201\Rule{\Gamma\vdash\vf\Hab\fbind{\vx}{\vS}{\vT}\hg\Gamma\vdash\vs\Hab\vS}
202{\Gamma\vdash\vf\;\vs\Hab\vT[\vs/\vx]} % \LET\;\vx\Hab\vS\;\defq\;\vs\;\IN\;\vT}
205\Rule{\Gamma;\lam{\vx}{\vS}\vdash\ve\Hab\vT\hg\Gamma\proves\fbind{\vx}{\vS}{\vT}\Hab\Type_n}
206{\Gamma\vdash\lam{\vx}{\vS}.\ve\Hab\fbind{\vx}{\vS}{\vT}}
209\Rule{\Gamma;\all{\vx}{\vS}\vdash\vT\Hab\Type_m\hg\Gamma\vdash\vS\Hab\Type_n}
210{\Gamma\vdash\fbind{\vx}{\vS}{\vT}\Hab\Type_p}
211\;(\exists\vp.\vm\le\vp,\;\vn\le\vp)
214\Rule{\begin{array}{c}\Gamma\proves\ve_1\Hab\vS\hg
215 \Gamma;\LET\;\vx\defq\ve_1\Hab\vS\proves\ve_2\Hab\vT\\
216 \Gamma\proves\vS\Hab\Type_n\hg
217 \Gamma;\LET\;\vx\defq\ve_1\Hab\vS\proves\vT\Hab\Type_n\end{array}
219{\Gamma\vdash\LET\;\vx\defq\ve_1\Hab\vS\SC\;\ve_2\Hab
221%\Let\;\vx\Hab\vS\defq\ve_1\;\IN\;\vT}
225\Rule{\Gamma\proves\vx\Hab\vA\hg\Gamma\proves\vA'\Hab\Type_n\hg
226 \Gamma\proves\vA\cumul\vA'}
227 {\Gamma\proves\vx\Hab\vA'}
230{Typing rules for \TT{}}
235\Rule{\Gamma\proves\vS\converts\vT}
236{\Gamma\proves\vS\cumul\vT}
238\Axiom{\Gamma\proves\Type_n\cumul\Type_{n+1}}
240\Rule{\Gamma\proves\vR\cumul\vS\hg\Gamma\proves\vS\cumul\vT}
241{\Gamma\proves\vR\cumul\vT}
243\Rule{\Gamma\proves\vS_1\converts\vS_2\hg\Gamma;\vx\Hab\vS_1\proves\vT_1\cumul\vT_2}
244{\Gamma\proves\all{\vx}{\vS_1}\SC\vT_1\cumul\all{\vx}{\vS_2}{\vT_2}}
251\subsection{Inductive Families}
253\label{sect:inductivefams}
255Inductive families \cite{dybjer1994inductive} are a form of simultaneously
256defined collection of algebraic data types which can be parameterised over
257\remph{values} as well as types. An inductive family is declared
258in a similar style to a Haskell GADT declaration~\cite{pj2006gadts}
260follows, using vector notation, $\tx$, to indicate a
261sequence of zero or more $\vx$ (i.e., $\vx_1,\vx_2,\ldots,\vx_n$):
265\Data\hg\TC{T}\;(\tx\Hab\ttt)\Hab\vt\hg\Where\hg
266\DC{c}_1\Hab\vt\;\mid\;\ldots\;\mid\;\DC{c}_n\Hab\vt
270Constructors may take recursive arguments in the family $\TC{T}$, which may be
271higher order. Higher order recursive arguments may be computed from any type
272which does not involve $\TC{T}$ itself. This restriction is known as
273\demph{strict positivity} and ensures that recursive arguments of the
274constructor are structurally smaller than the value itself.
276For example, the \Idris{} data type \tTC{Nat} would be declared in \TT{} as follows:
279\Data\hg\Nat\Hab\Type\hg\Where\hg\Z\Hab\Nat\;\mid\;\suc\Hab\fbind{\vk}{\Nat}{\Nat}
282A data type may have zero or more parameters (which are invariant
283across a structure) and a number of indices, given by the type. For
284example, the \TT{} equivalent of \tTC{List} is parameterised over its element type:
288\Data\hg\List\:(\va\Hab\Type)\Hab\Type\hg\Where\\
291& \nil\Hab\List\;\va\\
292\mid & (\cons)\Hab\fbind{\vx}{\va}{\fbind{\vxs}{\List\;\va}{\List\;\va}}
298parameterised over values. Using this, we can declare the type of
299vectors (lists with length), where the empty list is statically known
300to have length zero, and the non empty list is statically known to
301have a non zero length. The \TT{} equivalent of \tTC{Vect} is parameterised over its element type,
302like $\List$, but \remph{indexed} over its length. Note also that the length
303index $\vk$ is given \remph{explicitly}.
307\Data\hg\Vect\;(\va\Hab\Type)\Hab\Nat\to\Type\hg\Where \\
309& \nil\Hab\Vect\;\va\;\Z\\
310\mid & (\cons)\Hab\fbind{\vk}{\Nat}{
311\fbind{\vx}{\va}{\fbind{\vxs}{\Vect\;\va\;\vk}{\Vect\;\va\;(\suc\;\vk)}}
317\subsection{Pattern matching definitions}
321%\subsubsection{Syntax}
324A pattern matching definition for a function named $\FN{f}$ takes the following form,
325consisting of a type declaration followed by one or more pattern clauses:
330\pat{\tx_1}{\ttt_1}\SC\FN{f}\;\ttt_1\;=\;\vt_1\\
332\pat{\tx_n}{\ttt_n}\SC\FN{f}\;\ttt_n\;=\;\vt_n\\
336A pattern clause consists of a list of pattern variable bindings, introduced by
338and a left and right hand side, both of which
339are \TT{} expressions. Each side is type checked relative to the variable bindings,
340and the types of each side must be convertible. Additionally, the
341left hand side must take the form of $\FN{f}$ applied to a number of \TT{} expressions,
342and the number of arguments must be the same in each clause. The right hand
343sides may include applications of $\FN{f}$, i.e. pattern matching definitions may
344be recursive. Termination analysis is implemented separately. The validity of a pattern
345clause is defined by the following rule:
349\Gamma;\lam{\tx}{\tU}\proves\FN{f}\;\tts\Hab\vS\hg
350\Gamma;\lam{\tx}{\tU}\proves\ve\Hab\vT\hg
351\Gamma\proves\vS\converts\vT}
353\Gamma\proves\pat{\tx}{\tU}\SC\FN{f}\;\tts\;=\;\ve\;\RW{valid}
357A valid pattern matching definition effectively extends \TT{} with a new
358constant, with the given type (extending the initial typing rules given in
359Section \ref{sect:typerules}) and reduction behaviour (extending the initial
360reduction rules given in Section \ref{sect:evaluation}).
361Patterns are separated into the accessible patterns (variables and constructor
362forms which may be inspected) and inaccessible patterns, following
363Agda~\cite{norell2007thesis} then implemented by compilation into case
364trees~\cite{Augustsson1985}.
366% \subsubsection{Semantics}
368% Matching on an expression proceeds by comparing the expression to
369% each match clause in order, resulting in either:
372% \item \demph{Success}, with pattern variables mapping to expressions
373% \item \demph{Failure}, with matching continuing by proceeding to the next match clause
374% \item Matching being \demph{blocked}, for example by attempting to match a variable
375% against a constructor pattern. In this case, no reduction occurs, because instantiating
376% the variable may provide enough information for the clause to match.
379% % Pat(x args) => x (Pat' args)
383% In order to implement pattern matching, we must separate the \remph{accessible} and
384% \remph{inaccessible} patterns. A pattern is \demph{accessible} (that is, it is possible
385% to match against it) if it is constructor headed, or a variable. Inaccessible patterns
386% are converted to ``match anything'' patterns. Clauses are converted to matchable pattern
387% clauses with the $\MO{Clause}$ operation, given in Figure \ref{mkclause}.
388% We extend the vector notation to meta-operations: the notation $\vec{\MO{Pat}}$ lifts the
389% $\MO{Pat}$ operation across a list of arguments.
394% & \MO{Clause} & (\pat{\tx}{\tU}\SC\FN{f}\;\tts\;=\;\ve)
395% & \MoRet{\FN{f}\;(\vec{\MO{Pat}}\;\tts)\;=\;\ve}
399% & \MO{Pat} & (\vx\;\tts) & \MoRet{\vx\;(\vec{\MO{Pat}}\;\tts)
400% \hg\mbox{(if $\MO{Con}\;\vx$ and $\MO{Arity}\;\vx = \MO{Length}\;\tts$)}} \\
401% & \MO{Pat} & \vx & \MoRet{\vx} \hg\mbox(if $\vx$ is a pattern variable)\\
402% & \MO{Pat} & \cdot & \MoRet{\_} \hg\mbox(in all other cases)\\
406% {Building matchable pattern clauses}
410% % Match (c args, c args') => Match' (args, args')
411% % Match (c args, x) => Blocked
412% % Match (x, t) => Success (x => t)
413% % Match (_, t) => Success ()
415% \newcommand{\Blocked}{\mathsf{Blocked}}
416% \newcommand{\Success}{\mathsf{Success}}
417% \newcommand{\Failure}{\mathsf{Failure}}
419% Pattern matching is invoked by the evaluator on encountering a function with
420% a pattern matching definition applied to some arguments. If successful, pattern
421% matching returns a new expression, which can then be reduced further.
422% Figure \ref{pmatch} gives the semantics of pattern matching a collection of
424% $\tc$ against an expression $\ve$. $\MO{Match}$ attempts to match each clause in
425% turn against $\ve$. If matching a clause returns $\Success$ or $\Blocked$, then
426% matching terminates. If matching a clause returns $\Failure$, then matching proceeds
427% with the next clause. The algorithm uses the following meta-operations:
430% \item $\MO{Con}\;\vx$, which returns true if $\vx$ is a constructor name
431% \item $\MO{Arity}\;\vx$, which, if $\vx$ is a constructor name, returns the number of arguments
433% \item $\MO{Length}\;\tts$, which returns the length of the vector $\tts$
440% & \MO{MatchArg} & (\vx\;\tts) & (\vx\;\tts')
441% & \MoRet{\vec{\MO{MatchArg}}\;\tts\;\tts'\hg\mbox{(if $\MO{Con}\;\vx$)}}\\
442% & \MO{MatchArg} & (\vx\;\tts) & \vx & \MoRet{\Blocked} \\
443% & \MO{MatchArg} & \vx & \vt & \MoRet{\Success\;(\vx\mapsto\vt)} \\
444% & \MO{MatchArg} & \_ & \vt & \MoRet{\Success\;()} \\
445% & \MO{MatchArg} & \cdot & \cdot & \MoRet{\Failure}
449% & \MO{MatchClause} & (\vf\;\tp = \ve) & (\vf\;\tts) &
452% \Success\;\ve[\tx/\tv]\hg\mbox{(if $\vec{\MO{MatchArg}}\;\tp\;\tts \mq \Success\;(\tx,\tv)$)}\\
453% \Blocked\;\;\;\hg\hg\mbox{(if $\vec{\MO{MatchArg}}\;\tp\;\tts \mq \Blocked$)}\\
454% \Failure\;\;\;\;\;\hg\hg\mbox{(if $\vec{\MO{MatchArg}}\;\tp\;\tts \mq \Failure$)}\\
457% & \MO{MatchClause} & (\vf\;\tp = \ve) & \cdot & \MoRet{\Failure} \\
461% & \MO{Match} & (\vc ; \tc) & \ve &
464% \Success\;\vx\;\;\hg\mbox{(if $\MO{MatchClause}\;\vc\;\ve \mq \Success\;\vx)$} \\
465% \Blocked\hg\;\;\;\;\mbox{(if $\MO{MatchClause}\;\vc\;\ve \mq \Blocked)$} \\
466% \MO{Match}\;\tc\;\ve\hg\mbox{(otherwise)}
469% & \MO{Match} & \cdot & \ve & \MoRet{\Failure}
473% {Pattern matching semantics}
476% By convention, we write the application of a meta-operation $\MO{Op}$
477% across a vector $\tx$ as $\vec{\MO{Op}}\;\tx$.
478% In practice, for efficiency, pattern matching is implemented by compiling the match clauses to
479% a tree of case expressions~\cite{Augustsson1985}.
481\subsection{Metatheory}
485\mbox{\textbf{Church-Rosser}} &
487\mbox{If}\hg\Gamma\proves\vs\converts\vt \\
488\mbox{then there is a common reduct $\vr$ such that}\;\\
489\Gamma\proves\vs\reducesto\vr\hg\Gamma\proves\vt\reducesto\vr
493\mbox{\textbf{Subject Reduction}} &
495\mbox{If} & \Gamma\proves\vs\Hab\vS\hg\Gamma\proves\vs\reduces\vt\\
496\mbox{then}& \Gamma\proves\vt\Hab\vS
502\mbox{If} & \Gamma_0,\LET\;\vx\defq\vs\Hab\vS,\Gamma_1\proves\vt\Hab\vT\\
503\mbox{then} & \Gamma_0, \Gamma_1[\vs/\vx]\proves\vt[\vs/\vx]\Hab\vT[\vs/\vx]
507\mbox{\textbf{Strengthening}} &
509\mbox{If} & \Gamma_0,\mathcal{B}(\vx, \vT),\Gamma_1\proves\vs\Hab\vS
510\hg\vx\not\in\Gamma_1,\vs,\vS\\
511\mbox{then} & \Gamma_0,\Gamma_1\proves\vs\Hab\vS\\
512(\mbox{where} & \mathcal{B}(\vx, \vT) \proves \vx\Hab\vT)
517{Metatheoretic properties of \TT{}}
520We conjecture that \TT{} respects the usual metatheoretic properties, as shown in
521Figure \ref{metatheory}. Specifically: the \demph{Church-Rosser} property
522(i.e. that distinct reduction sequences lead to the same normal form);
523\demph{subject reduction} (i.e. that computation preserves type); the
524\demph{cut} property (i.e. that $\RW{let}$-bound terms may be substituted into
525their scope); and \demph{strengthening} (i.e. that removing unused definitions
526from scope does not affect type checking).
528One property which is noticeably absent is \demph{strong normalisation}.
529Although desirable to preserve termination and decidability of type checking,
530we allow diverging terms for pragmatic reasons as \Idris{} is primarily a
531programming language rather than a theorem prover. Nevertheless, we do
532\emph{check} for totality in order to be sure which terms are safe to
533evaluate at compile time.
535\subsection{Totality checking}
537In order to ensure termination of type checking we must distinguish terms for
538which evaluation definitely terminates, and those which may diverge. \TT{}
539takes a simple but pragmatic and effective approach to termination checking:
540any functions which do not satisfy a syntactic constraint on recursive calls
541are marked as \emph{partial}. Additionally, any function which calls a partial
542function or uses a data type which is not strictly positive is also marked as
543partial. We use the size change principle~\cite{Lee2001} to determine whether
544(possibly mutually defined) recursive functions are guaranteed to
546\TT{} also marks functions which do not cover
547all possible inputs as partial. This totality checking is independent of the
548rest of the type theory, and can be extended.
550This approach, separating the termination requirement from the type theory,
551means that an \Idris{} programmer makes the decision about the importance of
552totality for each function rather than having the totality requirement imposed
555\subsection{From \Idris{} to \TT{}}
557\TT{} is a very small language, consisting only of data declarations and pattern matching
558function definitions. There is no significant innovation in the design of \TT{}, and this
559is a deliberate choice --- it is a combination of small, well-understood components.
560The kernel of the \TT{} implementation, consisting of a type checker, evaluator and
561pattern match compiler, is less than 1000 lines of Haskell code. If we are confident
562in the correctness of the kernel of \TT{}, and any higher level language feature
563can be translated into \TT{}, we can be more confident of the correctness of the high
564level language implementation than if it were implemented directly.
566The process of elaborating a high level language into a core type theory like \TT{} is,
567however, less well understood, and presents several challenges depending on the
568features of the high level language.
569%Elaboration has been implemented in various different ways,
570%for example in Agda~\cite{norell2007thesis} and Epigram~\cite{McBride2004a}.
572\subsubsection{Example Elaboration}
574Recall the following \Idris{} function:
580this to \TT{}, we must resolve the implicit arguments, and make the type class explicit.
581The first step is to make the implicit arguments explicit, using a placeholder
582to stand for the arguments we have not yet resolved. The type class argument is
583also treated as an implicit argument, to which we give the name \texttt{c}:
585\begin{SaveVerbatim}{vAddImp}
587vAdd : (a : _) -> (n : _) -> Num a -> Vect a n -> Vect a n -> Vect a n
588vAdd _ _ c (Nil _) (Nil _) = (Nil _)
589vAdd _ _ c ((::) _ _ x xs) ((::) _ _ y ys)
590 = (::) _ _ ((+) _ x y) (vAdd _ _ _ xs ys)
595Next, we resolve the implicit arguments. Each implicit argument can only take
596one value for this program to be type correct --- these are solved by a unification
599\begin{SaveVerbatim}{vAddImpSolve}
601vAdd : (a : Type) -> (n : Nat) -> Num a -> Vect a n -> Vect a n -> Vect a n
602vAdd a O c (Nil a) (Nil a) = Nil a
603vAdd a (S k) c ((::) a k x xs) ((::) a k y ys)
604 = (::) a k ((+) c x y) (vAdd a k c xs ys)
607\useverb{vAddImpSolve}
609Finally, to build the \TT{} definition, we need to find the type of each
610pattern variable and state it explicitly. This leads to the following
611\TT{} definition, switching to \TT{} notation from the ASCII \Idris{}
616\FN{vAdd} \Hab(\va\Hab\Type)\to(\vn\Hab\Nat)\to\TC{Num}\;\va\to
617 \Vect\;\va\;\vn\to\Vect\;\va\;\vn\to\Vect\;\va\;\vn\\
618\RW{var}\;\va\Hab\Type,\;\vc\Hab\TC{Num}\;\va\SC\\
619\hg\FN{vAdd} \; \va \; \Z \; \vc \; (\DC{Nil}\;\va) \; (\DC{Nil}\;\va) \;
622\va\Hab\Type,\;\vk\Hab\Nat,\;\vc\Hab\TC{Num}\;\va,\\
623\vx\Hab\va,\;\vxs\Hab\Vect\;\va\;\vk,\;
624\vy\Hab\va,\;\vys\Hab\Vect\;\va\;\vk
627\FN{vAdd} \; \va \; (\suc\;\vk) \; \vc
628 \; ((\DC{::})\;\va\;\vk\;\vx\;\vxs)
629 \; ((\DC{::})\;\va\;\vk\;\vy\;\vys)
631 \hg\hg\cq\:((\DC{::})\;\va\;\vk\;((+)\;\vc\;\vx\;\vy)\; (\FN{vAdd}\;\va\;\vk\;\vc\;\vxs\;\vys))
636\subsubsection{An Observation: Programming vs Theorem Proving}
638\Idris{} programs may contain several high level constructs not present in \TT{}, such
639as implicit arguments, type classes, \texttt{where} clauses, pattern matching \texttt{let}
640and \texttt{case} constructs. We would like the high level language to be as expressive
641as possible, while remaining possible to translate to \TT{}.
643Before considering how to achieve this, we make an observation about the distinction between
644programming and theorem proving with dependent types, and appropriate mechanisms for
645constructing programs and theorems:
648\item \remph{Pattern matching} is a convenient abstraction for humans to write
649programs, in that it allows a programmer to express exactly the computational
650behaviour of a function.
651\item \remph{Tactics}, such as those used in the Coq theorem
652prover~\cite{Bertot2004}, are a convenient abstraction for building proofs and
653programs by \remph{refinement}.
656The idea behind the \Idris{} elaborator, therefore, is to use the high level
657program to direct \demph{tactics} to build \TT{} programs by refinement. The
658elaborator is implemented as a Haskell monad capturing proof state, with a
659collection of tactics for updating and refining the proof state. The remainder
660of this paper describes this elaborator and demonstrates how it is used to
661implement 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