@@ -94,9 +94,19 @@ names may reduce.
9494
9595\label{sect:evaluation}
9696
97−Evaluation of \TT{} is defined by contraction schemes, given in Figure
98−\ref{ttcontract}. \demph{Contraction}, relative to a context $\Gamma$, is given
99−by one of the following schemes:
97+There are two distinct phases in which \TT{} evaluation occurs, namely
98+\demph{compile-time} and \demph{run-time}. Compile-time evaluation is primarily
99+to support type-checking, in which equivalence of two terms (or types) is
100+determined by comparing their normal forms. It is important that terms are
101+strongly normalising at compile-time, so any pattern matching definition which
102+is not guaranteed to be total does not reduce. In this section we discuss
103+compile-time evaluation; run-time evaluation differs in that there is no
104+reduction under binders, types and duplicated values have been
105+erased~\cite{Brady2003}, and non-normalising definitions may reduce.
106+
107+Compile-time evaluation of \TT{} is defined by contraction schemes, given in
108+Figure \ref{ttcontract}. \demph{Contraction}, relative to a context $\Gamma$,
109+is given by one of the following schemes:
100110
101111\begin{itemize}
102112\item $\beta$-contraction, which substitutes a value applied to a $\lambda$-binding for
@@ -267,12 +277,11 @@ defined collection of algebraic data types which can be parameterised over
267277\remph{values} as well as types. An inductive family is declared
268278in a similar style to a Haskell GADT declaration~\cite{pj2006gadts}
269279as
270−follows, using vector notation, $\tx$, to indicate a
271−sequence of zero or more $\vx$ (i.e., $\vx_1,\vx_2,\ldots,\vx_n$):
280+follows:
272281
273282\DM{
274283\AR{
275−\Data\hg\TC{T}\;(\tx\Hab\ttt)\Hab\vt\hg\Where\hg
284+\Data\hg\TC{T}\Hab\vt\hg\Where\hg
276285\DC{D}_1\Hab\vt\;\mid\;\ldots\;\mid\;\DC{D}_n\Hab\vt
277286}
278287}
@@ -280,7 +289,10 @@ sequence of zero or more $\vx$ (i.e., $\vx_1,\vx_2,\ldots,\vx_n$):
280289A constructor $\TC{D}$ of a family $\TC{T}$ must return a value in the family
281290$\TC{T}$.
282291It may take recursive arguments in the family $\TC{T}$ which may be
283−higher order. That is, recursive arguments have types of the form
292+higher order.
293+Using vector notation, $\tx$, to indicate a
294+sequence of zero or more $\vx$ (i.e., $\vx_1,\vx_2,\ldots,\vx_n$),
295+recursive arguments have types of the form
284296
285297\DM{
286298\all{\vx_1}{\vS_1}\SC\ldots\all{\vx_n}{\vS_n}\SC\TC{T}\:\ty
@@ -301,8 +313,8 @@ For example, the \Idris{} data type \tTC{Nat} would be declared in \TT{} as foll
301313}
302314
303315A data type may have zero or more parameters (which are invariant
304−across a structure) and a number of indices, given by the type. For
305−example, the \TT{} equivalent of \tTC{List} is parameterised over its element type:
316+across a structure) and a number of indices, given by the type. For example,
317+the \TT{} equivalent of \tTC{List} is parameterised over its element type:
306318
307319\DM{
308320\AR{
@@ -316,7 +328,7 @@ example, the \TT{} equivalent of \tTC{List} is parameterised over its element ty
316328}
317329
318330Types can be
319−parameterised over values. Using this, we can declare the type of
331+parameterised or indexed over values. Using this, we can declare the type of
320332vectors (lists with length), where the empty list is statically known
321333to have length zero, and the non empty list is statically known to
322334have a non zero length. The \TT{} equivalent of \tTC{Vect} is parameterised over its element type,
@@ -362,7 +374,7 @@ and the types of each side must be convertible. Additionally, the
362374left hand side must take the form of $\FN{f}$ applied to a number of \TT{} expressions,
363375and the number of arguments must be the same in each clause. The right hand
364376sides may include applications of $\FN{f}$, i.e. pattern matching definitions may
365−be recursive. Termination analysis is implemented separately. The validity of a pattern
377+be recursive. The validity of a pattern
366378clause is defined by the following rule:
367379
368380\DM{
@@ -375,14 +387,19 @@ clause is defined by the following rule:
375387}
376388}
377389
390+Patterns are separated into the accessible patterns (variables and constructor
391+forms which may be inspected) and inaccessible patterns, following
392+Agda~\cite{norell2007thesis} then implemented by compilation into case
393+trees~\cite{Augustsson1985}. Non-terminating definitions are permitted, but do
394+not reduce at compile-time, which means in particular that they cannot be used
395+to construct proofs.
396+Termination analysis is implemented separately.
397+
378398A valid pattern matching definition effectively extends \TT{} with a new
379399constant, with the given type (extending the initial typing rules given in
380400Section \ref{sect:typerules}) and reduction behaviour (extending the initial
381401reduction rules given in Section \ref{sect:evaluation}).
382−Patterns are separated into the accessible patterns (variables and constructor
383−forms which may be inspected) and inaccessible patterns, following
384−Agda~\cite{norell2007thesis} then implemented by compilation into case
385−trees~\cite{Augustsson1985}.
402+
386403
387404% \subsubsection{Semantics}
388405%
@@ -532,26 +549,37 @@ trees~\cite{Augustsson1985}.
532549\mbox{then} & \Gamma_0,\Gamma_1\proves\vs\Hab\vS\\
533550(\mbox{where} & \mathcal{B}(\vx, \vT) \proves \vx\Hab\vT)
534551\end{array}
552+\medskip
553+\\
554+\mbox{\textbf{Strong normalisation}} &
555+\begin{array}{ll}
556+\mbox{If} & \Gamma\proves\vt\Hab\vT\\
557+\mbox{then} & \vt\:\mbox{is strongly normalising}\\
558+\end{array}
535559\\
536560\end{array}
537561}
538562{Metatheoretic properties of \TT{}}
539563{metatheory}
540564
541−We conjecture that \TT{} respects the usual metatheoretic properties, as shown in
565+We conjecture that \TT{} respects the usual metatheoretic properties,
566+as shown in
542567Figure \ref{metatheory}. Specifically: the \demph{Church-Rosser} property
543568(i.e. that distinct reduction sequences lead to the same normal form);
544569\demph{subject reduction} (i.e. that computation preserves type); the
545570\demph{cut} property (i.e. that $\RW{let}$-bound terms may be substituted into
546571their scope); and \demph{strengthening} (i.e. that removing unused definitions
547572from scope does not affect type checking).
573+\demph{Strong normalisation} holds at compile-time because pattern matching
574+definitions which cannot be shown to be terminating do not have compile-time
575+reduction behaviour.
548576
549−One property which is noticeably absent is \demph{strong normalisation}.
550−Although desirable to preserve termination and decidability of type checking,
551−we allow diverging terms for pragmatic reasons as \Idris{} is primarily a
552−programming language rather than a theorem prover. Nevertheless, we do
553−\emph{check} for totality in order to be sure which terms are safe to
554−evaluate at compile time.
577+%One property which is noticeably absent is \demph{strong normalisation}.
578+%Although desirable to preserve termination and decidability of type checking,
579+%we allow diverging terms for pragmatic reasons as \Idris{} is primarily a
580+%programming language rather than a theorem prover. Nevertheless, we do
581+%\emph{check} for totality in order to be sure which terms are safe to
582+%evaluate at compile time.
555583
556584\subsection{Totality checking}
557585
@@ -607,7 +635,8 @@ also treated as an implicit argument, to which we give the name \texttt{c}:
607635
608636\begin{SaveVerbatim}{vAddImp}
609637
610−vAdd : (a : _) -> (n : _) -> Num a -> Vect n a -> Vect n a -> Vect n a
638+vAdd : (a : _) -> (n : _) ->
639+ Num a -> Vect n a -> Vect n a -> Vect n a
611640vAdd _ _ c (Nil _) (Nil _) = (Nil _)
612641vAdd _ _ c ((::) _ _ x xs) ((::) _ _ y ys)
613642 = (::) _ _ ((+) _ x y) (vAdd _ _ _ xs ys)
@@ -621,7 +650,8 @@ algorithm:
621650
622651\begin{SaveVerbatim}{vAddImpSolve}
623652
624−vAdd : (a : Type) -> (n : Nat) -> Num a -> Vect n a -> Vect n a -> Vect n a
653+vAdd : (a : Type) -> (n : Nat) ->
654+ Num a -> Vect n a -> Vect n a -> Vect n a
625655vAdd a O c (Nil a) (Nil a) = Nil a
626656vAdd a (S k) c ((::) a k x xs) ((::) a k y ys)
627657 = (::) a k ((+) c x y) (vAdd a k c xs ys)