@@ -0,0 +1,347 @@
1+\section{Example: The Well-Typed Interpreter}
2+
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}:
9+
10+\begin{SaveVerbatim}{tydecl}
11+
12+data Ty = TyInt | TyBool | TyFun Ty Ty;
13+
14+\end{SaveVerbatim}
15+\useverb{tydecl}
16+
17+\noindent
18+We can write a function to translate these representations to a concrete \Idris{}
19+type:
20+
21+\begin{SaveVerbatim}{interpty}
22+
23+interpTy : Ty -> Set;
24+interpTy TyInt = Int;
25+interpTy TyBool = Bool;
26+interpTy (TyFun A T) = interpTy A -> interpTy T;
27+
28+\end{SaveVerbatim}
29+\useverb{interpty}
30+
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:
36+
37+\begin{SaveVerbatim}{usingg}
38+
39+using (G:Vect Ty n)
40+
41+\end{SaveVerbatim}
42+\useverb{usingg}
43+
44+\noindent
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:
47+
48+\begin{SaveVerbatim}{exprdecl}
49+
50+data Expr : Vect Ty n -> Ty -> Set
51+
52+\end{SaveVerbatim}
53+\useverb{exprdecl}
54+
55+\noindent
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
58+constructor in turn.
59+
60+\begin{SaveVerbatim}{exprty}
61+
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;
65+
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 ->
72+ Expr G c
73+ | If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a;
74+
75+\end{SaveVerbatim}
76+\codefig{exprty}{Expression representation}
77+
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:
82+
83+\begin{SaveVerbatim}{hastype}
84+
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;
88+
89+\end{SaveVerbatim}
90+\useverb{hastype}
91+
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:
97+
98+\begin{SaveVerbatim}{varcon}
99+
100+Var : HasType i G t -> Expr G t
101+
102+\end{SaveVerbatim}
103+\useverb{varcon}
104+
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.
110+
111+\noindent
112+A value carries a concrete representation of an integer:
113+
114+\begin{SaveVerbatim}{valcon}
115+
116+Val : (x : Int) -> Expr G TyInt
117+
118+\end{SaveVerbatim}
119+\useverb{valcon}
120+
121+\noindent
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:
124+
125+\begin{SaveVerbatim}{lamcon}
126+
127+Lam : Expr (a :: G) t -> Expr G (TyFun a t)
128+
129+\end{SaveVerbatim}
130+\useverb{lamcon}
131+
132+\noindent
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}:
136+
137+\begin{SaveVerbatim}{appcon}
138+
139+App : Expr G (TyFun a t) -> Expr G a -> Expr G t
140+
141+\end{SaveVerbatim}
142+\useverb{appcon}
143+
144+\noindent
145+We allow arbitrary binary operators, where the type of the operator
146+informs what the types of the arguments must be:
147+
148+\begin{SaveVerbatim}{opcon}
149+
150+Op : (interpTy a -> interpTy b -> interpTy c) -> Expr G a -> Expr G b ->
151+ Expr G c
152+
153+\end{SaveVerbatim}
154+\useverb{opcon}
155+
156+\noindent
157+Finally, if expressions make a choice given a boolean. Each branch must
158+have the same type:
159+
160+\begin{SaveVerbatim}{ifcon}
161+
162+If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a;
163+
164+\end{SaveVerbatim}
165+\useverb{ifcon}
166+
167+\noindent
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:
174+
175+\begin{SaveVerbatim}{envtype}
176+
177+data Env : Vect Ty n -> Set where
178+ Nil : Env Nil
179+ | (::) : interpTy a -> Env G -> Env (a :: G);
180+
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;
184+
185+\end{SaveVerbatim}
186+\useverb{envtype}
187+
188+\begin{SaveVerbatim}{interpdef}
189+
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);
198+
199+\end{SaveVerbatim}
200+\codefig{interpdef}{Intepreter definition}
201+
202+\noindent
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:
206+
207+\begin{SaveVerbatim}{interpty}
208+
209+interp : Env G -> Expr G t -> interpTy t;
210+
211+\end{SaveVerbatim}
212+\useverb{interpty}
213+
214+\noindent
215+To translate a variable, we simply look it up in the environment:
216+
217+\begin{SaveVerbatim}{varinterp}
218+
219+interp env (Var i) = lookup i env;
220+
221+\end{SaveVerbatim}
222+\useverb{varinterp}
223+
224+\noindent
225+To translate a value, we just return the concrete representation of the value:
226+
227+\begin{SaveVerbatim}{valinterp}
228+
229+interp env (Val x) = x;
230+
231+\end{SaveVerbatim}
232+\useverb{valinterp}
233+
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:
237+
238+\begin{SaveVerbatim}{laminterp}
239+
240+interp env (Lam sc) = \x => interp (x :: env) sc;
241+
242+\end{SaveVerbatim}
243+\useverb{laminterp}
244+
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
247+type:
248+
249+\begin{SaveVerbatim}{appinterp}
250+
251+interp env (App f s) = (interp env f) (interp env s);
252+
253+\end{SaveVerbatim}
254+\useverb{appinterp}
255+
256+\noindent
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
260+directly.
261+
262+\begin{SaveVerbatim}{opinterp}
263+
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);
267+
268+\end{SaveVerbatim}
269+\useverb{opinterp}
270+
271+\noindent
272+We can make some simple test functions. Firstly, adding two inputs
273+\texttt{$\backslash$x. $\backslash$y. y + x} is written as follows:
274+
275+\begin{SaveVerbatim}{addtest}
276+
277+add : Expr G (TyFun TyInt (TyFun TyInt TyInt));
278+add = Lam (Lam (Op (+) (Var stop) (Var (pop stop))));
279+
280+\end{SaveVerbatim}
281+\useverb{addtest}
282+
283+\noindent
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:
287+
288+\begin{SaveVerbatim}{lazyapp}
289+
290+app : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t;
291+app = \f, a => App f a;
292+
293+\end{SaveVerbatim}
294+\useverb{lazyapp}
295+
296+\noindent
297+Then \texttt{fact}
298+(i.e. \texttt{$\backslash$x. if (x == 0) then 1 else (fact (x-1) * x)})
299+is written as follows:
300+
301+\begin{SaveVerbatim}{facttest}
302+
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)))
306+ (Var stop)));
307+
308+\end{SaveVerbatim}
309+\useverb{facttest}
310+
311+To finish, we write a \texttt{main} program which interprets the factorial function
312+on user input:
313+
314+\begin{SaveVerbatim}{factmain}
315+
316+main : IO ();
317+main = do { putStr "Enter a number: ";
318+ x <- getLine;
319+ print (interp [] fact (prim__strToInt x));
320+ };
321+
322+\end{SaveVerbatim}
323+\useverb{factmain}
324+
325+\noindent
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}.
329+
330+\begin{SaveVerbatim}{factrun}
331+
332+$ idris interp.idr
333+ ____ __ _
334+ / _/___/ /____(_)____
335+ / // __ / ___/ / ___/ Version 0.9
336+ _/ // /_/ / / / (__ ) http://www.idris-lang.org/
337+ /___/\__,_/_/ /_/____/ Type :? for help
338+
339+Type checking ./interp.idr
340+*interp> :exec interp
341+Enter a number: 6
342+720
343+*interp>
344+
345+\end{SaveVerbatim}
346+\codefig{factrun}{Running the well-typed interpreter}
347+