@@ -1,12 +1,12 @@
11\section{The Core Type Theory}
22
3−High level \Idris{} programs, as described in Section \ref{sect:hll} are
3+High level \Idris{} programs, as described in Section \ref{sect:hll}, are
44\remph{elaborated} to a small core language, \TT{}, then type checked.
55\TT{} is a dependently typed $\lambda$-calculus with inductive families
66and pattern matching definitions similar to UTT~\cite{luo1994}, and building
77on an earlier implementation, \Ivor{}~\cite{Brady2006b}.
88We keep the
9−core language as small as is reasonable, which has several advantages: it is
9+core language as small as is reasonably possible, which has several advantages: it is
1010easy to type check, since type checking dependent type theory is well understood
1111~\cite{loh2010tutorial}; and it is easy to transform, optimise and compile. Keeping
1212the core language small increases our confidence that these important components of
@@ -53,6 +53,12 @@ inferred by the machine~\cite{pollack1990implicit}.
5353{\TT{} expression syntax}
5454{ttsyn}
5555
56+A \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.
59+Before defining these, let us define the semantics of \TT{}
60+expressions.
61+
5662\subsection{\TT{} semantics}
5763
5864The static and dynamic semantics of \TT{} are defined mutually, since
@@ -71,7 +77,7 @@ $\LET$ binding:
7177
7278\subsubsection{Evaluation}
7379
74−Conceptually, evaluation of \TT{} is defined by contraction schemes, given in Figure
80+Evaluation of \TT{} is defined by contraction schemes, given in Figure
7581\ref{ttcontract}. \demph{Contraction}, relative to a context $\Gamma$, is given
7682by one of the following schemes:
7783
@@ -88,6 +94,10 @@ is the smallest equivalence relation closed under reduction. If $\Gamma\proves\v
8894then $\vy$ can be obtained from $\vx$ by a finite, possibly empty, sequence of
8995contractions and reversed contractions. Terms which are convertible are also said to
9096be computationally equal.
97+The evaluator can also be extended by defining pattern matching functions, which
98+will be described in more detail in Section \ref{sect:patdefs}. In principle, pattern
99+matching functions can be understood as extending the core language with high level
100+reduction rules.
91101
92102\FFIG{
93103\begin{array}{lc}
@@ -106,29 +116,21 @@ be computationally equal.
106116{\TT{} contraction schemes}
107117{ttcontract}
108118
109−\subsubsection{Cumulativity}
110119
111−Figure \ref{cumul} gives the \demph{cumulativity} relation.
112−
113−\FFIG{
114−\begin{array}{c}
115−\Rule{\Gamma\proves\vS\converts\vT}
116−{\Gamma\proves\vS\cumul\vT}
117−\hg
118−\Axiom{\Gamma\proves\Type_n\cumul\Type_{n+1}}
119−\\
120−\Rule{\Gamma\proves\vR\cumul\vS\hg\Gamma\proves\vS\cumul\vT}
121−{\Gamma\proves\vR\cumul\vT}
122−\\
123−\Rule{\Gamma\proves\vS_1\converts\vS_2\hg\Gamma;\vx\Hab\vS_1\proves\vT_1\cumul\vT_2}
124−{\Gamma\proves\all{\vx}{\vS_1}\SC\vT_1\cumul\all{\vx}{\vS_2}{\vT_2}}
125−\end{array}
126−}
127−{Cumulativity}
128−{cumul}
129120
130121\subsubsection{Typing rules}
131122
123+The type inference rules for \TT{} expressions are given in Figure \ref{typerules}.
124+These rules use the \demph{cumulativity} relation, defined in
125+Figure \ref{cumul}. The type of types, $\Type_i$ is parameterised by a universe level,
126+to prevent Girard's paradox~\cite{coquand1986analysis}. Cumulativity allows programs at
127+lower universe levels to inhabit higher universe levels. In practice, universe levels
128+can be left implicit (and will be left implicit in the rest of this paper) ---
129+the type checker generates a graph of constraints between universe levels (such
130+as that produced by the $\mathsf{Forall}$ typing rule) and checks that there
131+are no cycles. Otherwise, the typing rules are standard and type inference can
132+be implemented in the usual way~\cite{loh2010tutorial}.
133+
132134\FFIG{\begin{array}{c}
133135\mathsf{Type}\:
134136\Rule{\Gamma\proves\RW{valid}}
@@ -187,11 +189,29 @@ Figure \ref{cumul} gives the \demph{cumulativity} relation.
187189{Typing rules for \TT{}}
188190{typerules}
189191
192+\FFIG{
193+\begin{array}{c}
194+\Rule{\Gamma\proves\vS\converts\vT}
195+{\Gamma\proves\vS\cumul\vT}
196+\hg
197+\Axiom{\Gamma\proves\Type_n\cumul\Type_{n+1}}
198+\\
199+\Rule{\Gamma\proves\vR\cumul\vS\hg\Gamma\proves\vS\cumul\vT}
200+{\Gamma\proves\vR\cumul\vT}
201+\\
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}}
204+\end{array}
205+}
206+{Cumulativity}
207+{cumul}
208+
190209\subsection{Inductive Families}
191210
211+\label{sect:inductivefams}
212+
192213Inductive families \cite{dybjer1994inductive} are a form of simultaneously
193−defined collection of algebraic data types (such as Haskell
194−\texttt{data} declarations) which can be parametrised over
214+defined collection of algebraic data types which can be parametrised over
195215\remph{values} as well as types. An inductive family is declared
196216in a similar style to a Haskell GADT declaration~\cite{pj2006gadts}
197217as
@@ -253,6 +273,155 @@ index $\vk$ is given \remph{explicitly}.
253273
254274\subsection{Pattern matching definitions}
255275
276+\label{sect:patdefs}
277+
278+\subsubsection{Syntax}
279+
280+A pattern matching definition for a function named $\FN{f}$ takes the following form,
281+consisting of a type declaration followed by one or more pattern clauses:
282+
283+\DM{
284+\AR{
285+\FN{f}\Hab\vt\\
286+\pat{\tx_1}{\ttt_1}\SC\FN{f}\:\ttt_1\:=\:\vt_1\\
287+\ldots\\
288+\pat{\tx_n}{\ttt_n}\SC\FN{f}\:\ttt_n\:=\:\vt_n\\
289+}
290+}
291+
292+A pattern clause consists of a list of pattern variable bindings,
293+and a left and right hand side, both of which
294+are \TT{} expressions. Each side is type checked relative to the variable bindings,
295+and the types of each side must convert. Additionally, the
296+left hand side must take the form of $\FN{f}$ applied to a number of \TT{} expressions,
297+and the number of arguments must be the same in each clause. The right hand
298+sides may include applications of $\FN{f}$, i.e. pattern matching definitions may
299+be recursive. Termination analysis is implemented separately. The validity of a pattern
300+clause is defined by the following rule:
301+
302+\DM{
303+\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}
307+{
308+\Gamma\proves\pat{\tx}{\tU}\SC\FN{f}\:\tts\:=\:\ve\:\RW{valid}
309+}
310+}
311+
312+\subsubsection{Semantics}
313+
314+Matching on an expression proceeds by comparing the expression to
315+each match clause in order, resulting in either:
316+
317+\begin{itemize}
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
321+against a constructor pattern. In this case, no reduction occurs, because instantiating
322+the variable may provide enough information for the clause to match.
323+\end{itemize}
324+
325+% Pat(x args) => x (Pat' args)
326+% Pat (x) => x
327+% Pat _ => _
328+
329+In 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
331+to match against it) if it is constructor headed, or a variable. Inaccessible patterns
332+are converted to ``match anything'' patterns. We convert clauses to matchable pattern
333+clauses with the $\MO{Clause}$ operation, given in Figure \ref{mkclause}.
334+We extend the telescope notation to meta-operations: the notation $\vec{\MO{Pat}}$ lifts the
335+$\MO{Pat}$ operation across a list of arguments.
336+
337+\FFIG{
338+\AR{
339+\PA{\A}{
340+& \MO{Clause} & (\pat{\tx}{\tU}\SC\FN{f}\:\tts\:=\:\ve)
341+ & \MoRet{\FN{f}\:(\vec{\MO{Pat}}\:\tts)\:=\:\ve}
342+}
343+\medskip\\
344+\PA{\A}{
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)\\
349+}
350+}
351+}
352+{Building matchable pattern clauses}
353+{mkclause}
354+
355+
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 ()
360+
361+\newcommand{\Blocked}{\mathsf{Blocked}}
362+\newcommand{\Success}{\mathsf{Success}}
363+\newcommand{\Failure}{\mathsf{Failure}}
364+
365+Pattern matching is invoked by the evaluator on encountering a function with
366+a pattern matching definition applied to some arguments. If successful, pattern
367+matching returns a new expression, which can then be reduced further.
368+Figure \ref{pmatch} gives the semantics of pattern matching a collection of
369+matchable clauses
370+$\tc$ against an expression $\ve$. $\MO{Match}$ attempts to match each clause in
371+turn against $\ve$. If matching a clause returns $\Success$ or $\Blocked$, then
372+matching terminates. If matching a clause returns $\Failure$, then matching proceeds
373+with the next clause. The algorithm uses the following meta-operations:
374+
375+\begin{itemize}
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
378+$\vx$ requires.
379+\item $\MO{Length}\:\tts$, which returns the length of the telescope $\tts$
380+\end{itemize}
381+
382+
383+\FFIG{
384+\AR{
385+\PA{\A\A}{
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}
392+}
393+\medskip\\
394+\PA{\A\A}{
395+& \MO{MatchClause} & (\vf\:\tp = \ve) & (\vf\:\tts) &
396+ \MoRet{
397+ \AR{
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$)}\\
401+ }
402+ } \\
403+& \MO{MatchClause} & (\vf\:\tp = \ve) & \cdot & \MoRet{\Failure} \\
404+}
405+\medskip\\
406+\PA{\A\A}{
407+& \MO{Match} & (\vc ; \tc) & \ve &
408+ \MoRet{
409+ \AR{
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)}
413+ }
414+ } \\
415+& \MO{Match} & \cdot & \ve & \MoRet{\Failure}
416+}
417+}
418+}
419+{Pattern matching semantics}
420+{pmatch}
421+
422+In practice, for efficiency, pattern matching is implemented by compiling the match clauses to
423+a tree of case expressions~\cite{Augustsson1985}.
424+
256425\subsection{The Development Calculus \TTdev}
257426
258427\TTdev{} is \TT{} extended with hole binders, Oleg-style~\cite{McBride1999}.