@@ -0,0 +1,347 @@
1+\section{Example: The Well-Typed Interpreter}
3+In this chapter, we'll use the features we've seen so far to write a larger
4+example, an interpreter for a simple functional programming language, with
5+variables, function application, binary operators and an \texttt{if...then...else}
6+construct. We will use the dependent type system to ensure that any programs
7+which can be represented are well-typed. First, let us define the types in the
8+language. We have integers, booleans, and functions, represented by \texttt{Ty}:
10+\begin{SaveVerbatim}{tydecl}
12+data Ty = TyInt | TyBool | TyFun Ty Ty;
18+We can write a function to translate these representations to a concrete \Idris{}
21+\begin{SaveVerbatim}{interpty}
25+interpTy TyBool = Bool;
26+interpTy (TyFun A T) = interpTy A -> interpTy T;
31+We're going to define a representation of our language in such a way that only
32+well-typed programs can be represented. We'll index the representations of
33+expressions by their type and the types of local variables (the context), which
34+we'll be using regularly as an implicit argument, so we define everything
35+in a \texttt{using} block:
37+\begin{SaveVerbatim}{usingg}
45+The full representation of expressions is given in Figure \ref{exprty}. They are
46+indexed by the types of the local variables, and the type of the expression itself:
48+\begin{SaveVerbatim}{exprdecl}
50+data Expr : Vect Ty n -> Ty -> Set
56+Since expressions are indexed by their type, we can read the typing rules of
57+the language from the definitions of the constructors. Let us look at each
60+\begin{SaveVerbatim}{exprty}
62+data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Set where
63+ stop : HasType fO (t :: G) t
64+ | pop : HasType k G t -> HasType (fS k) (u :: G) t;
66+data Expr : Vect Ty n -> Ty -> Set where
67+ Var : HasType i G t -> Expr G t
68+ | Val : (x : Int) -> Expr G TyInt
69+ | Lam : Expr (a :: G) t -> Expr G (TyFun a t)
70+ | App : Expr G (TyFun a t) -> Expr G a -> Expr G t
71+ | Op : (interpTy a -> interpTy b -> interpTy c) -> Expr G a -> Expr G b ->
73+ | If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a;
76+\codefig{exprty}{Expression representation}
78+We use a nameless representation for variables --- they are \emph{de Bruijn indexed}.
79+Variables are represented by a proof of their membership in the context,
80+\texttt{HasType i G T}, which is a proof that variable \texttt{i} in context
81+\texttt{G} has type \texttt{T}. This is defined as follows:
83+\begin{SaveVerbatim}{hastype}
85+data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Set where
86+ stop : HasType fO (t :: G) t
87+ | pop : HasType k G t -> HasType (fS k) (u :: G) t;
92+We can treat \remph{stop} as a proof that the most recently defined variable is well-typed,
93+and \remph{pop n} as a proof that, if the \texttt{n}th most recently defined variable is
94+well-typed, so is the \texttt{n+1}th. In practice, this means we use \texttt{pop} to
95+refer to the most recently defined variable, \texttt{pop stop} to refer to the next, and so on,
96+via the \texttt{Var} constructor:
98+\begin{SaveVerbatim}{varcon}
100+Var : HasType i G t -> Expr G t
105+So, in an expression \texttt{$\backslash$x. $\backslash$y. x y},
106+the variable \texttt{x} would have a de Bruijn index
107+of 1, represented as \texttt{pop stop}, and \texttt{y 0}, represented
108+as \texttt{stop}. We find these by counting the number of lambdas between the
109+definition and the use.
112+A value carries a concrete representation of an integer:
114+\begin{SaveVerbatim}{valcon}
116+Val : (x : Int) -> Expr G TyInt
122+A lambda creates a function. In the scope of a function of type \texttt{a -> t}, there is
123+a new local variable of type \texttt{a}, which is expressed by the context index:
125+\begin{SaveVerbatim}{lamcon}
127+Lam : Expr (a :: G) t -> Expr G (TyFun a t)
133+Function application produces a value of type \texttt{t} given a function from
134+\texttt{a} to \texttt{t}
135+and a value of type \texttt{a}:
137+\begin{SaveVerbatim}{appcon}
139+App : Expr G (TyFun a t) -> Expr G a -> Expr G t
145+We allow arbitrary binary operators, where the type of the operator
146+informs what the types of the arguments must be:
148+\begin{SaveVerbatim}{opcon}
150+Op : (interpTy a -> interpTy b -> interpTy c) -> Expr G a -> Expr G b ->
157+Finally, if expressions make a choice given a boolean. Each branch must
160+\begin{SaveVerbatim}{ifcon}
162+If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a;
168+When we evaluate an \texttt{Expr}, we'll need to know the values in scope, as well as
169+their types. \texttt{Env} is an environment, indexed over the types in scope.
170+Since an environment is just another form of list, albeit with a strongly specified connection
171+to the vector of local variable types, we use the usual \texttt{::} and \texttt{Nil}
172+constructors so that we can use the usual list syntax. Given a proof that a variable
173+is defined in the context, we can then produce a value from the environment:
175+\begin{SaveVerbatim}{envtype}
177+data Env : Vect Ty n -> Set where
179+ | (::) : interpTy a -> Env G -> Env (a :: G);
181+lookup : HasType i G t -> Env G -> interpTy t;
182+lookup stop (x :: xs) = x;
183+lookup (pop k) (x :: xs) = lookup k xs;
188+\begin{SaveVerbatim}{interpdef}
190+interp : Env G -> Expr G t -> interpTy t;
191+interp env (Var i) = lookup i env;
192+interp env (Val x) = x;
193+interp env (Lam sc) = \x => interp (x :: env) sc;
194+interp env (App f s) = (interp env f) (interp env s);
195+interp env (Op op x y) = op (interp env x) (interp env y);
196+interp env (If x t e) = if (interp env x) then (interp env t)
197+ else (interp env e);
200+\codefig{interpdef}{Intepreter definition}
203+Given this, an interpreter (Figure \ref{interpdef})
204+is a function which translates an \texttt{Expr} into a
205+concrete \Idris{} value with respect to a specific environment:
207+\begin{SaveVerbatim}{interpty}
209+interp : Env G -> Expr G t -> interpTy t;
215+To translate a variable, we simply look it up in the environment:
217+\begin{SaveVerbatim}{varinterp}
219+interp env (Var i) = lookup i env;
225+To translate a value, we just return the concrete representation of the value:
227+\begin{SaveVerbatim}{valinterp}
229+interp env (Val x) = x;
234+Lambdas are more interesting. In this case, we construct a function which
235+interprets the scope of the lambda with a new value in the environment. So, a
236+function in the object language is translated to an \Idris{} function:
238+\begin{SaveVerbatim}{laminterp}
240+interp env (Lam sc) = \x => interp (x :: env) sc;
245+For an application, we interpret the function and its argument and apply it
246+directly. We know that interpreting \texttt{f} must produce a function, because of its
249+\begin{SaveVerbatim}{appinterp}
251+interp env (App f s) = (interp env f) (interp env s);
257+Operators and interpreters are, again, direct translations into the equivalent
258+\Idris{} constructs. For operators, we apply the function to its operands directly,
259+and for \texttt{If}, we apply the \Idris{} \texttt{if...then...else} construct
262+\begin{SaveVerbatim}{opinterp}
264+interp env (Op op x y) = op (interp env x) (interp env y);
265+interp env (If x t e) = if (interp env x) then (interp env t)
266+ else (interp env e);
272+We can make some simple test functions. Firstly, adding two inputs
273+\texttt{$\backslash$x. $\backslash$y. y + x} is written as follows:
275+\begin{SaveVerbatim}{addtest}
277+add : Expr G (TyFun TyInt (TyFun TyInt TyInt));
278+add = Lam (Lam (Op (+) (Var stop) (Var (pop stop))));
284+More interestingly, we can write a factorial function. First, we write a \emph{lazy}
285+version of the \texttt{App} constructor, so that the recursive branch will only
286+be evaluated if necessary:
288+\begin{SaveVerbatim}{lazyapp}
290+app : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t;
291+app = \f, a => App f a;
298+(i.e. \texttt{$\backslash$x. if (x == 0) then 1 else (fact (x-1) * x)})
299+is written as follows:
301+\begin{SaveVerbatim}{facttest}
303+fact : Expr G (TyFun TyInt TyInt);
304+fact = Lam (If (Op (==) (Var stop) (Val 0))
305+ (Val 1) (Op (*) (app fact (Op (-) (Var stop) (Val 1)))
311+To finish, we write a \texttt{main} program which interprets the factorial function
314+\begin{SaveVerbatim}{factmain}
317+main = do { putStr "Enter a number: ";
319+ print (interp [] fact (prim__strToInt x));
326+Here, \texttt{prim\_\_strToInt} is a primitive function which converts a string to
327+an integer, giving 0 if the input is invalid. An example run of this program
328+at the \Idris{} interactive environment is shown in Figure \ref{factrun}.
330+\begin{SaveVerbatim}{factrun}
334+ / _/___/ /____(_)____
335+ / // __ / ___/ / ___/ Version 0.9
336+ _/ // /_/ / / / (__ ) http://www.idris-lang.org/
337+ /___/\__,_/_/ /_/____/ Type :? for help
339+Type checking ./interp.idr
340+*interp> :exec interp
346+\codefig{factrun}{Running the well-typed interpreter}