@@ -1,12 +1,12 @@
1\section{The Core Type Theory}
1\section{The Core Type Theory}
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
4\remph{elaborated} to a small core language, \TT{}, then type checked.
4\remph{elaborated} to a small core language, \TT{}, then type checked.
5\TT{} is a dependently typed $\lambda$-calculus with inductive families
5\TT{} is a dependently typed $\lambda$-calculus with inductive families
6and pattern matching definitions similar to UTT~\cite{luo1994}, and building
6and pattern matching definitions similar to UTT~\cite{luo1994}, and building
7on an earlier implementation, \Ivor{}~\cite{Brady2006b}.
7on an earlier implementation, \Ivor{}~\cite{Brady2006b}.
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
10easy to type check, since type checking dependent type theory is well understood
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
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
12the core language small increases our confidence that these important components of
@@ -53,6 +53,12 @@ inferred by the machine~\cite{pollack1990implicit}.
53{\TT{} expression syntax}
53{\TT{} expression syntax}
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{}
56\subsection{\TT{} semantics}
62\subsection{\TT{} semantics}
58The static and dynamic semantics of \TT{} are defined mutually, since
64The static and dynamic semantics of \TT{} are defined mutually, since
@@ -71,7 +77,7 @@ $\LET$ binding:
72\subsubsection{Evaluation}
78\subsubsection{Evaluation}
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
75\ref{ttcontract}. \demph{Contraction}, relative to a context $\Gamma$, is given
81\ref{ttcontract}. \demph{Contraction}, relative to a context $\Gamma$, is given
76by one of the following schemes:
82by one of the following schemes:
@@ -88,6 +94,10 @@ is the smallest equivalence relation closed under reduction. If $\Gamma\proves\v
88then $\vy$ can be obtained from $\vx$ by a finite, possibly empty, sequence of
94then $\vy$ can be obtained from $\vx$ by a finite, possibly empty, sequence of
89contractions and reversed contractions. Terms which are convertible are also said to
95contractions and reversed contractions. Terms which are convertible are also said to
90be computationally equal.
96be 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
93\begin{array}{lc}
103\begin{array}{lc}
@@ -106,29 +116,21 @@ be computationally equal.
106{\TT{} contraction schemes}
116{\TT{} contraction schemes}
107{ttcontract}
117{ttcontract}
109−\subsubsection{Cumulativity}
111−Figure \ref{cumul} gives the \demph{cumulativity} relation.
115−\Rule{\Gamma\proves\vS\converts\vT}
116−{\Gamma\proves\vS\cumul\vT}
118−\Axiom{\Gamma\proves\Type_n\cumul\Type_{n+1}}
120−\Rule{\Gamma\proves\vR\cumul\vS\hg\Gamma\proves\vS\cumul\vT}
121−{\Gamma\proves\vR\cumul\vT}
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}}
130\subsubsection{Typing rules}
121\subsubsection{Typing rules}
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}.
132\FFIG{\begin{array}{c}
134\FFIG{\begin{array}{c}
133\mathsf{Type}\:
135\mathsf{Type}\:
134\Rule{\Gamma\proves\RW{valid}}
136\Rule{\Gamma\proves\RW{valid}}
@@ -187,11 +189,29 @@ Figure \ref{cumul} gives the \demph{cumulativity} relation.
187{Typing rules for \TT{}}
189{Typing rules for \TT{}}
188{typerules}
190{typerules}
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}}
190\subsection{Inductive Families}
209\subsection{Inductive Families}
211+\label{sect:inductivefams}
192Inductive families \cite{dybjer1994inductive} are a form of simultaneously
213Inductive families \cite{dybjer1994inductive} are a form of simultaneously
193−defined collection of algebraic data types (such as Haskell
214+defined collection of algebraic data types which can be parametrised over
194−\texttt{data} declarations) which can be parametrised over
195\remph{values} as well as types. An inductive family is declared
215\remph{values} as well as types. An inductive family is declared
196in a similar style to a Haskell GADT declaration~\cite{pj2006gadts}
216in a similar style to a Haskell GADT declaration~\cite{pj2006gadts}
@@ -253,6 +273,155 @@ index $\vk$ is given \remph{explicitly}.
254\subsection{Pattern matching definitions}
274\subsection{Pattern matching definitions}
278+\subsubsection{Syntax}
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:
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\\
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:
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}
314+Matching on an expression proceeds by comparing the expression to
315+each 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
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.
325+% Pat(x args) => x (Pat' args)
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.
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}}
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
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:
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}
422+In practice, for efficiency, pattern matching is implemented by compiling the match clauses to
423+a tree of case expressions~\cite{Augustsson1985}.
256\subsection{The Development Calculus \TTdev}
425\subsection{The Development Calculus \TTdev}
258\TTdev{} is \TT{} extended with hole binders, Oleg-style~\cite{McBride1999}.
427\TTdev{} is \TT{} extended with hole binders, Oleg-style~\cite{McBride1999}.