git.iko.soy/Idris-dev
on 293c8a2 help sign in
Idris-dev/tutorial/interp.tex
414 lines 12 kB history raw
1\section{Example: The Well-Typed Interpreter}
3\label{sect:interp}
5In this section, we'll use the features we've seen so far to write a larger
6example, an interpreter for a simple functional programming language, with
7variables, function application, binary operators and an \texttt{if...then...else}
8construct. We will use the dependent type system to ensure that any programs
9which can be represented are well-typed. First, let us define the types in the
10language. We have integers, booleans, and functions, represented by \texttt{Ty}:
12\begin{SaveVerbatim}{tydecl}
14data Ty = TyInt | TyBool | TyFun Ty Ty
16\end{SaveVerbatim}
17\useverb{tydecl}
19\noindent
20We can write a function to translate these representations to a concrete \Idris{}
21type --- remember that types are first class, so can be calculated just like
22any other value:
24\begin{SaveVerbatim}{interpty}
26interpTy : Ty -> Type
27interpTy TyInt = Int
28interpTy TyBool = Bool
29interpTy (TyFun A T) = interpTy A -> interpTy T
31\end{SaveVerbatim}
32\useverb{interpty}
34\noindent
35We're going to define a representation of our language in such a way that only
36well-typed programs can be represented. We'll index the representations of
37expressions by their type and the types of local variables (the context), which
38we'll be using regularly as an implicit argument, so we define everything
39in a \texttt{using} block:
41\begin{SaveVerbatim}{usingg}
43using (G:Vect Ty n)
45\end{SaveVerbatim}
46\useverb{usingg}
48\noindent
49The full representation of expressions is given in Figure \ref{exprty}. They are
50indexed by the types of the local variables, and the type of the expression itself:
52\begin{SaveVerbatim}{exprdecl}
54data Expr : Vect Ty n -> Ty -> Type
56\end{SaveVerbatim}
57\useverb{exprdecl}
59\noindent
60Since expressions are indexed by their type, we can read the typing rules of
61the language from the definitions of the constructors. Let us look at each
62constructor in turn.
64\begin{SaveVerbatim}{exprty}
66data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Type where
67 stop : HasType fO (t :: G) t
68 pop : HasType k G t -> HasType (fS k) (u :: G) t
70data Expr : Vect Ty n -> Ty -> Type where
71 Var : HasType i G t -> Expr G t
72 Val : (x : Int) -> Expr G TyInt
73 Lam : Expr (a :: G) t -> Expr G (TyFun a t)
74 App : Expr G (TyFun a t) -> Expr G a -> Expr G t
75 Op : (interpTy a -> interpTy b -> interpTy c) -> Expr G a -> Expr G b ->
76 Expr G c
77 If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a
79\end{SaveVerbatim}
80\codefig{exprty}{Expression representation}
82\noindent
83We use a nameless representation for variables --- they are \emph{de Bruijn indexed}.
84Variables are represented by a proof of their membership in the context,
85\texttt{HasType i G T}, which is a proof that variable \texttt{i} in context
86\texttt{G} has type \texttt{T}. This is defined as follows:
88\begin{SaveVerbatim}{hastype}
90data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Type where
91 stop : HasType fO (t :: G) t
92 pop : HasType k G t -> HasType (fS k) (u :: G) t
94\end{SaveVerbatim}
95\useverb{hastype}
97\noindent
98We can treat \remph{stop} as a proof that the most recently defined variable is well-typed,
99and \remph{pop n} as a proof that, if the \texttt{n}th most recently defined variable is
100well-typed, so is the \texttt{n+1}th. In practice, this means we use \texttt{stop} to
101refer to the most recently defined variable, \texttt{pop stop} to refer to the next, and so on,
102via the \texttt{Var} constructor:
104\begin{SaveVerbatim}{varcon}
106Var : HasType i G t -> Expr G t
108\end{SaveVerbatim}
109\useverb{varcon}
111\noindent
112So, in an expression \texttt{$\backslash$x. $\backslash$y. x y},
113the variable \texttt{x} would have a de Bruijn index
114of 1, represented as \texttt{pop stop}, and \texttt{y 0}, represented
115as \texttt{stop}. We find these by counting the number of lambdas between the
116definition and the use.
118\noindent
119A value carries a concrete representation of an integer:
121\begin{SaveVerbatim}{valcon}
123Val : (x : Int) -> Expr G TyInt
125\end{SaveVerbatim}
126\useverb{valcon}
128\noindent
129A lambda creates a function. In the scope of a function of type \texttt{a -> t}, there is
130a new local variable of type \texttt{a}, which is expressed by the context index:
132\begin{SaveVerbatim}{lamcon}
134Lam : Expr (a :: G) t -> Expr G (TyFun a t)
136\end{SaveVerbatim}
137\useverb{lamcon}
139\noindent
140Function application produces a value of type \texttt{t} given a function from
141\texttt{a} to \texttt{t}
142and a value of type \texttt{a}:
144\begin{SaveVerbatim}{appcon}
146App : Expr G (TyFun a t) -> Expr G a -> Expr G t
148\end{SaveVerbatim}
149\useverb{appcon}
151\noindent
152We allow arbitrary binary operators, where the type of the operator
153informs what the types of the arguments must be:
155\begin{SaveVerbatim}{opcon}
157Op : (interpTy a -> interpTy b -> interpTy c) -> Expr G a -> Expr G b ->
158 Expr G c
160\end{SaveVerbatim}
161\useverb{opcon}
163\noindent
164Finally, if expressions make a choice given a boolean. Each branch must
165have the same type:
167\begin{SaveVerbatim}{ifcon}
169If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a
171\end{SaveVerbatim}
172\useverb{ifcon}
174\noindent
175When we evaluate an \texttt{Expr}, we'll need to know the values in scope, as well as
176their types. \texttt{Env} is an environment, indexed over the types in scope.
177Since an environment is just another form of list, albeit with a strongly specified connection
178to the vector of local variable types, we use the usual \texttt{::} and \texttt{Nil}
179constructors so that we can use the usual list syntax. Given a proof that a variable
180is defined in the context, we can then produce a value from the environment:
182\begin{SaveVerbatim}{envtype}
184data Env : Vect Ty n -> Type where
185 Nil : Env Nil
186 (::) : interpTy a -> Env G -> Env (a :: G)
188lookup : HasType i G t -> Env G -> interpTy t
189lookup stop (x :: xs) = x
190lookup (pop k) (x :: xs) = lookup k xs
192\end{SaveVerbatim}
193\useverb{envtype}
195\begin{SaveVerbatim}{interpdef}
197interp : Env G -> Expr G t -> interpTy t
198interp env (Var i) = lookup i env
199interp env (Val x) = x
200interp env (Lam sc) = \x => interp (x :: env) sc
201interp env (App f s) = interp env f (interp env s)
202interp env (Op op x y) = op (interp env x) (interp env y)
203interp env (If x t e) = if interp env x then interp env t
204 else interp env e
206\end{SaveVerbatim}
207\codefig{interpdef}{Intepreter definition}
209\noindent
210Given this, an interpreter (Figure \ref{interpdef})
211is a function which translates an \texttt{Expr} into a
212concrete \Idris{} value with respect to a specific environment:
214\begin{SaveVerbatim}{interpty}
216interp : Env G -> Expr G t -> interpTy t
218\end{SaveVerbatim}
219\useverb{interpty}
221\noindent
222To translate a variable, we simply look it up in the environment:
224\begin{SaveVerbatim}{varinterp}
226interp env (Var i) = lookup i env
228\end{SaveVerbatim}
229\useverb{varinterp}
231\noindent
232To translate a value, we just return the concrete representation of the value:
234\begin{SaveVerbatim}{valinterp}
236interp env (Val x) = x
238\end{SaveVerbatim}
239\useverb{valinterp}
241\noindent
242Lambdas are more interesting. In this case, we construct a function which
243interprets the scope of the lambda with a new value in the environment. So, a
244function in the object language is translated to an \Idris{} function:
246\begin{SaveVerbatim}{laminterp}
248interp env (Lam sc) = \x => interp (x :: env) sc
250\end{SaveVerbatim}
251\useverb{laminterp}
253\noindent
254For an application, we interpret the function and its argument and apply it
255directly. We know that interpreting \texttt{f} must produce a function, because of its
256type:
258\begin{SaveVerbatim}{appinterp}
260interp env (App f s) = interp env f (interp env s)
262\end{SaveVerbatim}
263\useverb{appinterp}
265\noindent
266Operators and interpreters are, again, direct translations into the equivalent
267\Idris{} constructs. For operators, we apply the function to its operands directly,
268and for \texttt{If}, we apply the \Idris{} \texttt{if...then...else} construct
269directly.
271\begin{SaveVerbatim}{opinterp}
273interp env (Op op x y) = op (interp env x) (interp env y)
274interp env (If x t e) = if interp env x then interp env t
275 else interp env e
277\end{SaveVerbatim}
278\useverb{opinterp}
280\noindent
281We can make some simple test functions. Firstly, adding two inputs
282\texttt{$\backslash$x. $\backslash$y. y + x} is written as follows:
284\begin{SaveVerbatim}{addtest}
286add : Expr G (TyFun TyInt (TyFun TyInt TyInt))
287add = Lam (Lam (Op (+) (Var stop) (Var (pop stop))))
289\end{SaveVerbatim}
290\useverb{addtest}
292\noindent
293More interestingly, we can write a factorial function. First, we write a \emph{lazy}
294version of the \texttt{App} constructor, so that the recursive branch will only
295be evaluated if necessary:
297\begin{SaveVerbatim}{lazyapp}
299app : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t
300app = \f, a => App f a
302\end{SaveVerbatim}
303\useverb{lazyapp}
305\noindent
306The vertical bar annotation before the \texttt{f} argument indicates that this
307argument should be evaluated lazily when \texttt{app} is applied --- that is, the
308argument will be evaluated only when needed.
309Then \texttt{fact}
310(i.e. \texttt{$\backslash$x. if (x == 0) then 1 else (fact (x-1) * x)})
311is written as follows:
313\begin{SaveVerbatim}{facttest}
315fact : Expr G (TyFun TyInt TyInt)
316fact = Lam (If (Op (==) (Var stop) (Val 0))
317 (Val 1) (Op (*) (app fact (Op (-) (Var stop) (Val 1)))
318 (Var stop)))
320\end{SaveVerbatim}
321\useverb{facttest}
323To finish, we write a \texttt{main} program which interprets the factorial function
324on user input:
326\begin{SaveVerbatim}{factmain}
328main : IO ()
329main = do putStr "Enter a number: "
330 x <- getLine
331 print (interp [] fact (cast x))
333\end{SaveVerbatim}
334\useverb{factmain}
336\noindent
337Here, \texttt{cast} is an overloaded function which converts a value from one
338type to another if possible. Here, it converts a string to
339an integer, giving 0 if the input is invalid. An example run of this program
340at the \Idris{} interactive environment is shown in Figure \ref{factrun}.
342\begin{SaveVerbatim}[commandchars=^\{\}]{factrun}
344$ idris interp.idr
345 ____ __ _
346 / _/___/ /____(_)____
347 / // __ / ___/ / ___/ Version ^version{}
348 _/ // /_/ / / / (__ ) http://www.idris-lang.org/
349 /___/\__,_/_/ /_/____/ Type :? for help
351Type checking ./interp.idr
352*interp> :exec
353Enter a number: 6
354720
355*interp>
357\end{SaveVerbatim}
358\codefig{factrun}{Running the well-typed interpreter}
360\subsubsection*{Aside: \texttt{cast}}
362The prelude defines a type class \texttt{Cast} which allows conversion between
363types:
365\begin{SaveVerbatim}{castclass}
367class Cast from to where
368 cast : from -> to
370\end{SaveVerbatim}
371\useverb{castclass}
373\noindent
374It is a \emph{multi-parameter} type class, defining the source type and object
375type of the cast. It must be possible for the type checker to infer \remph{both}
376parameters at the point where the cast is applied.
377There are casts defined between all of the primitive types, as far as
378they make sense.
380\subsection{Unit testing}
382Recall the \texttt{so} data type:
384\useverb{sotype}
386\noindent
387This requires its parameter to be a \texttt{True} value. One simple application of this
388is to perform unit testing of functions at compile time. For example, we know that
389\texttt{4! = 24} so we can set up a test case as follows:
391\begin{SaveVerbatim}{unitTestFac}
393unitTestFac : so (interp [] fact 4 == 24)
394unitTestFac = oh
396\end{SaveVerbatim}
397\useverb{unitTestFac}
399\noindent
400For the program to compile, the test case must pass. If we change \texttt{24} to \texttt{25},
401say, we will get an error message like the following:
403\begin{SaveVerbatim}{unitTestErr}
405Type checking ./interp.idr
406interp.idr:64:Can't unify so True with so False
408Specifically:
409 Can't unify True with False
411\end{SaveVerbatim}
412\useverb{unitTestErr}