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}
80Evaluation of \TT{} is defined by contraction schemes, given in Figure
81\ref{ttcontract}. \demph{Contraction}, relative to a context $\Gamma$, is given
82by one of the following schemes:
85\item $\beta$-contraction, which substitutes a value applied to a $\lambda$-binding for
86the bound variable. We define $\beta$-constraction simply by replacing the $\lambda$-binding
88\item $\delta$-contraction, which replaces a $\LET$ bound variable with its value.
91\demph{Reduction} ($\reduces$) is the structural closure of contraction, and evaluation
92is ($\reducesto$) is the transitive closure of reduction. \demph{Conversion} ($\converts$)
93is the smallest equivalence relation closed under reduction. If $\Gamma\proves\vx\converts\vy$
94then $\vy$ can be obtained from $\vx$ by a finite, possibly empty, sequence of
95contractions and reversed contractions. Terms which are convertible are also said to
96be computationally equal.
97The evaluator can also be extended by defining pattern matching functions, which
98will be described in more detail in Section \ref{sect:patdefs}. In principle, pattern
99matching functions can be understood as extending the core language with high level
104\beta\mathrm{-contraction} &
106\Gamma\proves(\lam{\vx}{\vS}\SC\vt)\:\vs\leadsto\LET\:\vx\defq\vs\Hab\vS\SC\vt
108\delta\mathrm{-contraction} &
110\Gamma;\LET\:\vx\defq\vs\Hab\vS;\Gamma'
116{\TT{} contraction schemes}
121\subsubsection{Typing rules}
123The type inference rules for \TT{} expressions are given in Figure \ref{typerules}.
124These rules use the \demph{cumulativity} relation, defined in
125Figure \ref{cumul}. The type of types, $\Type_i$ is parameterised by a universe level,
126to prevent Girard's paradox~\cite{coquand1986analysis}. Cumulativity allows programs at
127lower universe levels to inhabit higher universe levels. In practice, universe levels
128can be left implicit (and will be left implicit in the rest of this paper) ---
129the type checker generates a graph of constraints between universe levels (such
130as that produced by the $\mathsf{Forall}$ typing rule) and checks that there
131are no cycles. Otherwise, the typing rules are standard and type inference can
132be implemented in the usual way~\cite{loh2010tutorial}.
134\FFIG{\begin{array}{c}
136\Rule{\Gamma\proves\RW{valid}}
137{\Gamma\vdash\Type_n\Hab\Type_{n+1}}
140\Rule{(\lam{\vx}{\vS})\in\Gamma}
141{\Gamma\vdash\vx\Hab\vS}
144\Rule{(\all{\vx}{\vS})\in\Gamma}
145{\Gamma\vdash\vx\Hab\vS}
148\Rule{(\LET\:\vx\Hab\vS\defq\vs)\in\Gamma}
149{\Gamma\vdash\vx\Hab\vS}
152%\Rule{(\pat{\vx}{\vS})\in\Gamma}
153%{\Gamma\vdash\vx\Hab\vS}
156%\Rule{(\pty{\vx}{\vS})\in\Gamma}
157%{\Gamma\vdash\vx\Hab\vS}
160\Rule{\Gamma\vdash\vf\Hab\fbind{\vx}{\vS}{\vT}\hg\Gamma\vdash\vs\Hab\vS}
161{\Gamma\vdash\vf\:\vs\Hab\vT[\vs/\vx]} % \LET\:\vx\Hab\vS\:\defq\:\vs\:\IN\:\vT}
164\Rule{\Gamma;\lam{\vx}{\vS}\vdash\ve\Hab\vT\hg\Gamma\proves\fbind{\vx}{\vS}{\vT}\Hab\Type_n}
165{\Gamma\vdash\lam{\vx}{\vS}.\ve\Hab\fbind{\vx}{\vS}{\vT}}
168\Rule{\Gamma;\all{\vx}{\vS}\vdash\vT\Hab\Type_m\hg\Gamma\vdash\vS\Hab\Type_n}
169{\Gamma\vdash\fbind{\vx}{\vS}{\vT}\Hab\Type_p}
170\:(\exists\vp.\vm\le\vp,\:\vn\le\vp)
173\Rule{\begin{array}{c}\Gamma\proves\ve_1\Hab\vS\hg
174 \Gamma;\LET\:\vx\defq\ve_1\Hab\vS\proves\ve_2\Hab\vT\\
175 \Gamma\proves\vS\Hab\Type_n\hg
176 \Gamma;\LET\:\vx\defq\ve_1\Hab\vS\proves\vT\Hab\Type_n\end{array}
178{\Gamma\vdash\LET\:\vx\defq\ve_1\Hab\vS\SC\:\ve_2\Hab
180%\Let\:\vx\Hab\vS\defq\ve_1\:\IN\:\vT}
184\Rule{\Gamma\proves\vx\Hab\vA\hg\Gamma\proves\vA'\Hab\Type_n\hg
185 \Gamma\proves\vA\cumul\vA'}
186 {\Gamma\proves\vx\Hab\vA'}
189{Typing rules for \TT{}}
194\Rule{\Gamma\proves\vS\converts\vT}
195{\Gamma\proves\vS\cumul\vT}
197\Axiom{\Gamma\proves\Type_n\cumul\Type_{n+1}}
199\Rule{\Gamma\proves\vR\cumul\vS\hg\Gamma\proves\vS\cumul\vT}
200{\Gamma\proves\vR\cumul\vT}
202\Rule{\Gamma\proves\vS_1\converts\vS_2\hg\Gamma;\vx\Hab\vS_1\proves\vT_1\cumul\vT_2}
203{\Gamma\proves\all{\vx}{\vS_1}\SC\vT_1\cumul\all{\vx}{\vS_2}{\vT_2}}
209\subsection{Inductive Families}
211\label{sect:inductivefams}
213Inductive families \cite{dybjer1994inductive} are a form of simultaneously
214defined collection of algebraic data types which can be parametrised over
215\remph{values} as well as types. An inductive family is declared
216in a similar style to a Haskell GADT declaration~\cite{pj2006gadts}
218follows, using the de Bruijn telescope notation, $\tx$, to indicate a
219sequence of zero or more $\vx$:
223\Data\hg\TC{T}\:(\tx\Hab\ttt)\Hab\vt\hg\Where\hg
224\DC{c}_1\Hab\vt\:\mid\:\ldots\:\mid\:\DC{c}_n\Hab\vt
228Constructors may take recursive arguments in the family
229$\TC{T}$. Furthermore these arguments may themselves be indexed by another type ---
230if such indices do not involve $\TC{T}$ then the constructor is
231\demph{strictly positive}, which ensures that recursive arguments of the
232constructor are structurally smaller than the value itself.
234For example, the \Idris{} data type \tTC{Nat} would be declared in \TT{} as follows:
237\Data\hg\Nat\Hab\Type\hg\Where\hg\Z\Hab\Nat\:\mid\:\suc\Hab\fbind{\vk}{\Nat}{\Nat}
240A data type may have zero or more parameters (which are invariant
241across a structure) and a number of indices, given by the type. For
242example, the \TT{} equivalent of \tTC{List} is parametrised over its element type:
246\Data\hg\List\:(\va\Hab\Type)\Hab\Type\hg\Where
248& \nil\Hab\List\:\va\\
249\mid & (\cons)\Hab\fbind{\vx}{\va}{\fbind{\vxs}{\List\:\va}{\List\:\va}}
255parametrised over values. Using this, we can declare the type of
256vectors (lists with length), where the empty list is statically known
257to have length zero, and the non empty list is statically known to
258have a non zero length. The \TT{} equivalent of \tTC{Vect} is parametrised over its element type,
259like $\List$, but \remph{indexed} over its length. Note also that the length
260index $\vk$ is given \remph{explicitly}.
264\Data\hg\Vect\:(\va\Hab\Type)\Hab\Nat\to\Type\hg\Where \\
266& \nil\Hab\Vect\:\va\:\Z\\
267\mid & (\cons)\Hab\fbind{\vk}{\Nat}{
268\fbind{\vx}{\va}{\fbind{\vxs}{\Vect\:\va\:\vk}{\Vect\:\va\:(\suc\:\vk)}}
274\subsection{Pattern matching definitions}
278\subsubsection{Syntax}
280A pattern matching definition for a function named $\FN{f}$ takes the following form,
281consisting of a type declaration followed by one or more pattern clauses:
286\pat{\tx_1}{\ttt_1}\SC\FN{f}\:\ttt_1\:=\:\vt_1\\
288\pat{\tx_n}{\ttt_n}\SC\FN{f}\:\ttt_n\:=\:\vt_n\\
292A pattern clause consists of a list of pattern variable bindings,
293and a left and right hand side, both of which
294are \TT{} expressions. Each side is type checked relative to the variable bindings,
295and the types of each side must convert. Additionally, the
296left hand side must take the form of $\FN{f}$ applied to a number of \TT{} expressions,
297and the number of arguments must be the same in each clause. The right hand
298sides may include applications of $\FN{f}$, i.e. pattern matching definitions may
299be recursive. Termination analysis is implemented separately. The validity of a pattern
300clause is defined by the following rule:
304\Gamma;\lam{\tx}{\tU}\proves\FN{f}\:\tts\Hab\vS\hg
305\Gamma;\lam{\tx}{\tU}\proves\ve\Hab\vT\hg
306\Gamma\proves\vS\converts\vT}
308\Gamma\proves\pat{\tx}{\tU}\SC\FN{f}\:\tts\:=\:\ve\:\RW{valid}
312\subsubsection{Semantics}
314Matching on an expression proceeds by comparing the expression to
315each match clause in order, resulting in either:
318\item \demph{Success}, with pattern variables mapping to expressions
319\item \demph{Failure}, with matching continuing by proceeding to the next match clause
320\item Matching being \demph{blocked}, for example by attempting to match a variable
321against a constructor pattern. In this case, no reduction occurs, because instantiating
322the variable may provide enough information for the clause to match.
325% Pat(x args) => x (Pat' args)
329In order to implement pattern matching, we must separate the \remph{accessible} and
330\remph{inaccessible} patterns. A pattern is \demph{accessible} (that is, it is possible
331to match against it) if it is constructor headed, or a variable. Inaccessible patterns
332are converted to ``match anything'' patterns. We convert clauses to matchable pattern
333clauses with the $\MO{Clause}$ operation, given in Figure \ref{mkclause}.
334We extend the telescope notation to meta-operations: the notation $\vec{\MO{Pat}}$ lifts the
335$\MO{Pat}$ operation across a list of arguments.
340& \MO{Clause} & (\pat{\tx}{\tU}\SC\FN{f}\:\tts\:=\:\ve)
341 & \MoRet{\FN{f}\:(\vec{\MO{Pat}}\:\tts)\:=\:\ve}
345& \MO{Pat} & (\vx\:\tts) & \MoRet{\vx\:(\vec{\MO{Pat}}\:\tts)
346 \hg\mbox{(if $\MO{Con}\:\vx$ and $\MO{Arity}\:\vx = \MO{Length}\:\tts$)}} \\
347& \MO{Pat} & \vx & \MoRet{\vx} \hg\mbox(if $\vx$ is a pattern variable)\\
348& \MO{Pat} & \cdot & \MoRet{\_} \hg\mbox(in all other cases)\\
352{Building matchable pattern clauses}
356% Match (c args, c args') => Match' (args, args')
357% Match (c args, x) => Blocked
358% Match (x, t) => Success (x => t)
359% Match (_, t) => Success ()
361\newcommand{\Blocked}{\mathsf{Blocked}}
362\newcommand{\Success}{\mathsf{Success}}
363\newcommand{\Failure}{\mathsf{Failure}}
365Pattern matching is invoked by the evaluator on encountering a function with
366a pattern matching definition applied to some arguments. If successful, pattern
367matching returns a new expression, which can then be reduced further.
368Figure \ref{pmatch} gives the semantics of pattern matching a collection of
370$\tc$ against an expression $\ve$. $\MO{Match}$ attempts to match each clause in
371turn against $\ve$. If matching a clause returns $\Success$ or $\Blocked$, then
372matching terminates. If matching a clause returns $\Failure$, then matching proceeds
373with the next clause. The algorithm uses the following meta-operations:
376\item $\MO{Con}\:\vx$, which returns true if $\vx$ is a constructor name
377\item $\MO{Arity}\:\vx$, which, if $\vx$ is a constructor name, returns the number of arguments
379\item $\MO{Length}\:\tts$, which returns the length of the telescope $\tts$
386& \MO{MatchArg} & (\vx\:\tts) & (\vx\:\tts')
387 & \MoRet{\vec{\MO{MatchArg}}\:\tts\:\tts'\hg\mbox{(if $\MO{Con}\:\vx$)}}\\
388& \MO{MatchArg} & (\vx\:\tts) & \vx & \MoRet{\Blocked} \\
389& \MO{MatchArg} & \vx & \vt & \MoRet{\Success\:(\vx\mapsto\vt)} \\
390& \MO{MatchArg} & \_ & \vt & \MoRet{\Success\:()} \\
391& \MO{MatchArg} & \cdot & \cdot & \MoRet{\Failure}
395& \MO{MatchClause} & (\vf\:\tp = \ve) & (\vf\:\tts) &
398 \Success\:\ve[\tx/\tv]\hg\mbox{(if $\vec{\MO{MatchArg}}\:\tp\:\tts \mq \Success\:(\tx,\tv)$)}\\
399 \Blocked\hg\mbox{(if $\vec{\MO{MatchArg}}\:\tp\:\tts \mq \Blocked$)}\\
400 \Failure\hg\mbox{(if $\vec{\MO{MatchArg}}\:\tp\:\tts \mq \Failure$)}\\
403& \MO{MatchClause} & (\vf\:\tp = \ve) & \cdot & \MoRet{\Failure} \\
407& \MO{Match} & (\vc ; \tc) & \ve &
410 \Success\:\vx\hg\mbox{(if $\MO{MatchClause}\:\vc\:\ve \mq \Success\:\vx)$} \\
411 \Blocked\hg\mbox{(if $\MO{MatchClause}\:\vc\:\ve \mq \Blocked)$} \\
412 \MO{Match}\:\tc\:\ve\hg\mbox{(otherwise)}
415& \MO{Match} & \cdot & \ve & \MoRet{\Failure}
419{Pattern matching semantics}
422In practice, for efficiency, pattern matching is implemented by compiling the match clauses to
423a tree of case expressions~\cite{Augustsson1985}.
425\subsection{The Development Calculus \TTdev}
427\TTdev{} is \TT{} extended with hole binders, Oleg-style~\cite{McBride1999}.
429\subsection{The $\MO{Elab}$ meta-language}
433\item $\MO{Check}\:\vt\:\cq\:(\vt, \vt)$
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