Skip to content
Fetching contributors…
Cannot retrieve contributors at this time
598 lines (507 sloc) 21.4 KB
\section{The Core Type Theory}
High level \Idris{} programs, as described in Section \ref{sect:hll}, are
\remph{elaborated} to a small core language, \TT{}, then type checked.
\TT{} is a dependently typed $\lambda$-calculus with inductive families
and pattern matching definitions similar to UTT~\cite{luo1994}, and building
on an earlier implementation, \Ivor{}~\cite{Brady2006b}.
core language is kept as small as is reasonably possible, which has several advantages: it is
easy to type check, since type checking dependent type theory is well understood
~\cite{loh2010tutorial}; and it is easy to transform, optimise and compile. Keeping
the core language small increases confidence that these important components of
the language are correct. In this section, we describe \TT{} and
its semantics.
\subsection{\TT{} syntax}
The syntax of \TT{} expressions is given in Figure \ref{ttsyn}. This defines:
\item \demph{Terms}, $\vt$, which are variables, bindings, applications or constants.
\item \demph{Bindings}, $\vb$, which are lambda abstractions, let bindings, or function spaces.
\item \demph{Constants}, $\vc$, which are integer or string literals, or $\Type_i$, the
type of types, and may be extended with other primitives.
The function space $\all{\vx}{\vS}\SC\vT$ may also be written as $(\vx\Hab\vS)\to\vT$,
or $\vS\to\vT$ if $\vx$ is not free in $\vT$, to make the notation more consistent with
the high level language. Universe levels on sets ($\Type_i$) may be left implicit and
inferred by the machine~\cite{pollack1990implicit}.
\vt ::= & \vc & (\mbox{constant}) &
\hg\vb ::= & \lam{\vx}{\vt} & (\mbox{abstraction}) \\
\mid & \vx & (\mbox{variable}) &
\mid & \LET\:\vx\defq\vt\Hab\vt & (\mbox{let binding}) \\
\mid & \vb\SC\:\vt & (\mbox{binding}) &
\mid & \all{\vx}{\vt} & (\mbox{function space}) \\
\mid & \vt\;\vt & (\mbox{application}) &
% \mid & \pat{\vx}{\vt} & (\mbox{pattern variable}) \\
% & & &
% \mid & \pty{\vx}{\vt} & (\mbox{pattern type}) \\
\vc ::= & \Type_i & (\mbox{type universes}) \\
\mid & \vi & (\mbox{integer literal}) \\
\mid & \VV{str} & (\mbox{string literal}) \\
{\TT{} expression syntax}
A \TT{} program is a collection of \demph{inductive family} definitions (Section
\ref{sect:inductivefams}) and \demph{pattern matching} function definitions (Section
\ref{sect:patdefs}), as well as primitive operators on constants.
Before defining these, let us define the semantics of \TT{}
\subsection{\TT{} semantics}
The static and dynamic semantics of \TT{} are defined mutually, since
evaluation relies on a well-typed term, and type checking relies on
evaluation. Everything is defined relative
to a context, $\Gamma$. The empty context
is valid, as is a context extended with a $\lambda$, $\forall$ or
$\LET$ binding:
Evaluation of \TT{} is defined by contraction schemes, given in Figure
\ref{ttcontract}. \demph{Contraction}, relative to a context $\Gamma$, is given
by one of the following schemes:
\item $\beta$-contraction, which substitutes a value applied to a $\lambda$-binding for
the bound variable. We define $\beta$-contraction simply by replacing the $\lambda$-binding
with a $\LET$ binding.
\item $\delta$-contraction, which replaces a $\LET$ bound variable with its value.
The following contextual closure rule reduces a $\LET$ binding by creating
a $\delta$-reducible expression:
\demph{Reduction} ($\reduces$) is the structural closure of contraction, and evaluation
is ($\reducesto$) is the transitive closure of reduction. \demph{Conversion} ($\converts$)
is the smallest equivalence relation closed under reduction. If $\Gamma\proves\vx\converts\vy$
then $\vy$ can be obtained from $\vx$ by a finite, possibly empty, sequence of
contractions and reversed contractions. Terms which are convertible are also said to
be definitionally equal.
The evaluator can also be extended by defining pattern matching functions, which
will be described in more detail in Section \ref{sect:patdefs}. In principle, pattern
matching functions can be understood as extending the core language with high level
reduction rules.
\beta\mathrm{-contraction} &
} \\
\delta\mathrm{-contraction} &
{\TT{} contraction schemes}
\subsubsection{Typing rules}
The type inference rules for \TT{} expressions are given in Figure \ref{typerules}.
These rules use the \demph{cumulativity} relation, defined in
Figure \ref{cumul}. The type of types, $\Type_i$ is parameterised by a universe level,
to prevent Girard's paradox~\cite{coquand1986analysis}. Cumulativity allows programs at
lower universe levels to inhabit higher universe levels. In practice, universe levels
can be left implicit (and will be left implicit in the rest of this paper) ---
the type checker generates a graph of constraints between universe levels (such
as that produced by the $\mathsf{Forall}$ typing rule) and checks that there
are no cycles. Otherwise, the typing rules are standard and type inference can
be implemented in the usual way~\cite{loh2010tutorial}.
{\Gamma\vdash\vf\:\vs\Hab\vT[\vs/\vx]} % \LET\:\vx\Hab\vS\:\defq\:\vs\:\IN\:\vT}
{Typing rules for \TT{}}
\subsection{Inductive Families}
Inductive families \cite{dybjer1994inductive} are a form of simultaneously
defined collection of algebraic data types which can be parameterised over
\remph{values} as well as types. An inductive family is declared
in a similar style to a Haskell GADT declaration~\cite{pj2006gadts}
follows, using vector notation, $\tx$, to indicate a
sequence of zero or more $\vx$ (i.e., $\vx_1,\vx_2,\ldots,\vx_n$):
Constructors may take recursive arguments in the family
$\TC{T}$. Furthermore these arguments may themselves be indexed by another type ---
if such indices do not involve $\TC{T}$ then the constructor is
\demph{strictly positive}, which ensures that recursive arguments of the
constructor are structurally smaller than the value itself.
For example, the \Idris{} data type \tTC{Nat} would be declared in \TT{} as follows:
A data type may have zero or more parameters (which are invariant
across a structure) and a number of indices, given by the type. For
example, the \TT{} equivalent of \tTC{List} is parameterised over its element type:
& \nil\Hab\List\:\va\\
\mid & (\cons)\Hab\fbind{\vx}{\va}{\fbind{\vxs}{\List\:\va}{\List\:\va}}
Types can be
parameterised over values. Using this, we can declare the type of
vectors (lists with length), where the empty list is statically known
to have length zero, and the non empty list is statically known to
have a non zero length. The \TT{} equivalent of \tTC{Vect} is parameterised over its element type,
like $\List$, but \remph{indexed} over its length. Note also that the length
index $\vk$ is given \remph{explicitly}.
\Data\hg\Vect\:(\va\Hab\Type)\Hab\Nat\to\Type\hg\Where \\
& \nil\Hab\Vect\:\va\:\Z\\
\mid & (\cons)\Hab\fbind{\vk}{\Nat}{
\subsection{Pattern matching definitions}
A pattern matching definition for a function named $\FN{f}$ takes the following form,
consisting of a type declaration followed by one or more pattern clauses:
A pattern clause consists of a list of pattern variable bindings, introduced by
and a left and right hand side, both of which
are \TT{} expressions. Each side is type checked relative to the variable bindings,
and the types of each side must be convertible. Additionally, the
left hand side must take the form of $\FN{f}$ applied to a number of \TT{} expressions,
and the number of arguments must be the same in each clause. The right hand
sides may include applications of $\FN{f}$, i.e. pattern matching definitions may
be recursive. Termination analysis is implemented separately. The validity of a pattern
clause is defined by the following rule:
A valid pattern matching definition effectively extends \TT{} with a new constant,
with the given type (extending the initial typing rules given in Section \ref{sect:typerules})
and reduction behaviour (extending the initial reduction rules given in Section
Matching on an expression proceeds by comparing the expression to
each match clause in order, resulting in either:
\item \demph{Success}, with pattern variables mapping to expressions
\item \demph{Failure}, with matching continuing by proceeding to the next match clause
\item Matching being \demph{blocked}, for example by attempting to match a variable
against a constructor pattern. In this case, no reduction occurs, because instantiating
the variable may provide enough information for the clause to match.
% Pat(x args) => x (Pat' args)
% Pat (x) => x
% Pat _ => _
In order to implement pattern matching, we must separate the \remph{accessible} and
\remph{inaccessible} patterns. A pattern is \demph{accessible} (that is, it is possible
to match against it) if it is constructor headed, or a variable. Inaccessible patterns
are converted to ``match anything'' patterns. Clauses are converted to matchable pattern
clauses with the $\MO{Clause}$ operation, given in Figure \ref{mkclause}.
We extend the vector notation to meta-operations: the notation $\vec{\MO{Pat}}$ lifts the
$\MO{Pat}$ operation across a list of arguments.
& \MO{Clause} & (\pat{\tx}{\tU}\SC\FN{f}\:\tts\:=\:\ve)
& \MoRet{\FN{f}\:(\vec{\MO{Pat}}\:\tts)\:=\:\ve}
& \MO{Pat} & (\vx\:\tts) & \MoRet{\vx\:(\vec{\MO{Pat}}\:\tts)
\hg\mbox{(if $\MO{Con}\:\vx$ and $\MO{Arity}\:\vx = \MO{Length}\:\tts$)}} \\
& \MO{Pat} & \vx & \MoRet{\vx} \hg\mbox(if $\vx$ is a pattern variable)\\
& \MO{Pat} & \cdot & \MoRet{\_} \hg\mbox(in all other cases)\\
{Building matchable pattern clauses}
% Match (c args, c args') => Match' (args, args')
% Match (c args, x) => Blocked
% Match (x, t) => Success (x => t)
% Match (_, t) => Success ()
Pattern matching is invoked by the evaluator on encountering a function with
a pattern matching definition applied to some arguments. If successful, pattern
matching returns a new expression, which can then be reduced further.
Figure \ref{pmatch} gives the semantics of pattern matching a collection of
matchable clauses
$\tc$ against an expression $\ve$. $\MO{Match}$ attempts to match each clause in
turn against $\ve$. If matching a clause returns $\Success$ or $\Blocked$, then
matching terminates. If matching a clause returns $\Failure$, then matching proceeds
with the next clause. The algorithm uses the following meta-operations:
\item $\MO{Con}\:\vx$, which returns true if $\vx$ is a constructor name
\item $\MO{Arity}\:\vx$, which, if $\vx$ is a constructor name, returns the number of arguments
$\vx$ requires.
\item $\MO{Length}\:\tts$, which returns the length of the vector $\tts$
& \MO{MatchArg} & (\vx\:\tts) & (\vx\:\tts')
& \MoRet{\vec{\MO{MatchArg}}\:\tts\:\tts'\hg\mbox{(if $\MO{Con}\:\vx$)}}\\
& \MO{MatchArg} & (\vx\:\tts) & \vx & \MoRet{\Blocked} \\
& \MO{MatchArg} & \vx & \vt & \MoRet{\Success\:(\vx\mapsto\vt)} \\
& \MO{MatchArg} & \_ & \vt & \MoRet{\Success\:()} \\
& \MO{MatchArg} & \cdot & \cdot & \MoRet{\Failure}
& \MO{MatchClause} & (\vf\:\tp = \ve) & (\vf\:\tts) &
\Success\:\ve[\tx/\tv]\hg\mbox{(if $\vec{\MO{MatchArg}}\:\tp\:\tts \mq \Success\:(\tx,\tv)$)}\\
\Blocked\;\;\;\hg\hg\mbox{(if $\vec{\MO{MatchArg}}\:\tp\:\tts \mq \Blocked$)}\\
\Failure\;\;\;\;\;\hg\hg\mbox{(if $\vec{\MO{MatchArg}}\:\tp\:\tts \mq \Failure$)}\\
} \\
& \MO{MatchClause} & (\vf\:\tp = \ve) & \cdot & \MoRet{\Failure} \\
& \MO{Match} & (\vc ; \tc) & \ve &
\Success\;\vx\;\;\hg\mbox{(if $\MO{MatchClause}\:\vc\:\ve \mq \Success\:\vx)$} \\
\Blocked\hg\;\;\;\;\mbox{(if $\MO{MatchClause}\:\vc\:\ve \mq \Blocked)$} \\
} \\
& \MO{Match} & \cdot & \ve & \MoRet{\Failure}
{Pattern matching semantics}
By convention, we write the application of a meta-operation $\MO{Op}$
across a vector $\tx$ as $\vec{\MO{Op}}\:\tx$.
In practice, for efficiency, pattern matching is implemented by compiling the match clauses to
a tree of case expressions~\cite{Augustsson1985}.
\subsection{Totality checking}
In order to ensure termination of type checking
we must distinguish terms for which evaluation definitely terminates, and
those which may diverge. \TT{} takes a simple but pragmatic and
effective approach to termination
checking: any functions which do not satisfy a syntactic constraint on recursive
calls are marked as \emph{partial}. Additionally, any function which calls a partial
function or uses a data type which is not strictly positive is also marked as
partial. The syntactic constraint we use is that a recursive call in a pattern
clause must have an argument which is structurally smaller than an input argument
in the same position. \TT{} also marks functions which do not cover all possible
inputs as partial. This totality checking is independent of the rest of the type
theory, and can be extended.
This approach, separating the termination requirement from the type theory, means that
an \Idris{} programmer makes the decision about the importance of totality for each
function rather than having the totality requirement imposed by the type theory.
\subsection{From \Idris{} to \TT{}}
\TT{} is a very small language, consisting only of data declarations and pattern matching
function definitions. There is no significant innovation in the design of \TT{}, and this
is a deliberate choice --- it is a combination of small, well-understood components.
The kernel of the \TT{} implementation, consisting of a type checker, evaluator and
pattern match compiler, is less than 1000 lines of Haskell code. If we are confident
in the correctness of the kernel of \TT{}, and any higher level language feature
can be translated into \TT{}, we can be more confident of the correctness of the high
level language implementation than if it were implemented directly.
The process of elaborating a high level language into a core type theory like \TT{} is,
however, less well understood, and presents several challenges depending on the
features of the high level language.
%Elaboration has been implemented in various different ways,
%for example in Agda~\cite{norell2007thesis} and Epigram~\cite{McBride2004a}.
\subsubsection{Example Elaboration}
Recall the following \Idris{} function:
In order to elaborate
this to \TT{}, we must resolve the implicit arguments, and make the type class explicit.
The first step is to make the implicit arguments explicit, using a placeholder
to stand for the arguments we have not yet resolved. The type class argument is
also treated as an implicit argument, to which we give the name \texttt{c}:
vAdd : (a : _) -> (n : _) -> Num a -> Vect a n -> Vect a n -> Vect a n
vAdd _ _ c (Nil _) (Nil _) = (Nil _)
vAdd _ _ c ((::) _ _ x xs) ((::) _ _ y ys)
= (::) _ _ ((+) _ x y) (vAdd _ _ _ xs ys)
Next, we resolve the implicit arguments. Each implicit argument can only take
one value for this program to be type correct --- these are solved by a unification
vAdd : (a : Set) -> (n : Nat) -> Num a -> Vect a n -> Vect a n -> Vect a n
vAdd a O c (Nil a) (Nil a) = Nil a
vAdd a (S k) c ((::) a k x xs) ((::) a k y ys)
= (::) a k ((+) c x y) (vAdd a k c xs ys)
Finally, to build the \TT{} definition, we need to find the type of each pattern variable
and state it explicitly. This leads to the \TT{} definition in Figure \ref{ttvadd},
switching to \TT{} notation from the ASCII \Idris{} syntax.
\FN{vAdd} & \Hab(\va\Hab\Set)\to(\vn\Hab\Nat)\to\TC{Num}\:\va\to
\hg\FN{vAdd} & \va & \Z & \vc & (\DC{Nil}\;\va) & (\DC{Nil}\;\va) & \Ret{\DC{Nil}\;\va} \\
\hg\FN{vAdd} & \va & (\suc\;\vk) & \vc
& ((\DC{::})\;\va\;\vk\;\vx\;\vxs)
& ((\DC{::})\;\va\;\vk\;\vy\;\vys)
& \\
& & \MRet{5}{((\DC{::})\;\va\;\vk\;((+)\;\vc\;\vx\;\vy)\; (\FN{vAdd}\;\va\;\vk\;\vc\;\vxs\;\vys))}
{Pairwise addition of vectors in \TT{}}
\subsubsection{An observation}
\Idris{} programs may contain several high level constructs not present in \TT{}, such
as implicit arguments, type classes, \texttt{where} clauses, pattern matching \texttt{let}
and \texttt{case} constructs. We would like the high level language to be as expressive
as possible, while remaining possible to translate to \TT{}.
Before considering how to achieve this, we make an observation about the distinction between
programming and theorem proving with dependent types, and appropriate mechanisms for
constructing programs and theorems:
\item \remph{Pattern matching} is a convenient abstraction for humans to write programs,
in that it allows a programmer to express exactly the computational behaviour of a function.
\item \remph{Tactics}, such as those used in the Coq theorem prover~\cite{Bertot2004},
are a convenient abstraction for building proofs and programs by \remph{refinement}.
The idea behind the \Idris{} elaborator, therefore, is to use the high level program
to direct \demph{tactics} to build \TT{} programs by refinement. The
elaborator is implemented as an Embedded Domain Specific Language (EDSL) in Haskell.
The remainder
of this paper describes the EDSL and demonstrates how it is used to implement
all of the high level features of \Idris{}.
Something went wrong with that request. Please try again.