git.iko.soy/Idris-dev
on d1663cc help sign in
Idris-dev/tutorial/content/interp.tex
332 lines 11 kB history raw
1\section{Example: The Well-Typed Interpreter}
2\label{sect:interp}
4In this section, we'll use the features we've seen so far to write a larger
5example, an interpreter for a simple functional programming language, with
6variables, function application, binary operators and an \texttt{if...then...else}
7construct. We will use the dependent type system to ensure that any programs
8which can be represented are well-typed. First, let us define the types in the
9language. We have integers, booleans, and functions, represented by \texttt{Ty}:
11\begin{code}
12data Ty = TyInt | TyBool | TyFun Ty Ty
13\end{code}
15\noindent
16We can write a function to translate these representations to a concrete \Idris{}
17type --- remember that types are first class, so can be calculated just like
18any other value:
20\begin{code}
21interpTy : Ty -> Type
22interpTy TyInt = Int
23interpTy TyBool = Bool
24interpTy (TyFun A T) = interpTy A -> interpTy T
25\end{code}
27\noindent
28We're going to define a representation of our language in such a way that only
29well-typed programs can be represented. We'll index the representations of
30expressions by their type and the types of local variables (the context), which
31we'll be using regularly as an implicit argument, so we define everything
32in a \texttt{using} block:
34\begin{code}
35using (G:Vect n Ty)
36\end{code}
38\noindent
39The full representation of expressions is given in Figure \ref{exprty}. They are
40indexed by the types of the local variables, and the type of the expression itself:
42\begin{code}
43data Expr : Vect n Ty -> Ty -> Type
44\end{code}
46\noindent
47Since expressions are indexed by their type, we can read the typing rules of
48the language from the definitions of the constructors. Let us look at each
49constructor in turn.
51\begin{code}[caption={Expression representation},label=exprty]
52data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where
53 stop : HasType fZ (t :: G) t
54 pop : HasType k G t -> HasType (fS k) (u :: G) t
56data Expr : Vect n Ty -> Ty -> Type where
57 Var : HasType i G t -> Expr G t
58 Val : (x : Int) -> Expr G TyInt
59 Lam : Expr (a :: G) t -> Expr G (TyFun a t)
60 App : Expr G (TyFun a t) -> Expr G a -> Expr G t
61 Op : (interpTy a -> interpTy b -> interpTy c) -> Expr G a -> Expr G b ->
62 Expr G c
63 If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a
64\end{code}
66\noindent
67We use a nameless representation for variables --- they are \emph{de Bruijn indexed}.
68Variables are represented by a proof of their membership in the context,
69\texttt{HasType i G T}, which is a proof that variable \texttt{i} in context
70\texttt{G} has type \texttt{T}. This is defined as follows:
72\begin{code}
73data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where
74 stop : HasType fZ (t :: G) t
75 pop : HasType k G t -> HasType (fS k) (u :: G) t
76\end{code}
78\noindent
79We can treat \remph{stop} as a proof that the most recently defined variable is well-typed,
80and \remph{pop n} as a proof that, if the \texttt{n}th most recently defined variable is
81well-typed, so is the \texttt{n+1}th. In practice, this means we use \texttt{stop} to
82refer to the most recently defined variable, \texttt{pop stop} to refer to the next, and so on,
83via the \texttt{Var} constructor:
85\begin{code}
86Var : HasType i G t -> Expr G t
87\end{code}
89\noindent
90So, in an expression \texttt{$\backslash$x. $\backslash$y. x y},
91the variable \texttt{x} would have a de Bruijn index
92of 1, represented as \texttt{pop stop}, and \texttt{y 0}, represented
93as \texttt{stop}. We find these by counting the number of lambdas between the
94definition and the use.
96\noindent
97A value carries a concrete representation of an integer:
99\begin{code}
100Val : (x : Int) -> Expr G TyInt
101\end{code}
103\noindent
104A lambda creates a function. In the scope of a function of type \texttt{a -> t}, there is
105a new local variable of type \texttt{a}, which is expressed by the context index:
107\begin{code}
108Lam : Expr (a :: G) t -> Expr G (TyFun a t)
109\end{code}
111\noindent
112Function application produces a value of type \texttt{t} given a function from
113\texttt{a} to \texttt{t}
114and a value of type \texttt{a}:
116\begin{code}
117App : Expr G (TyFun a t) -> Expr G a -> Expr G t
118\end{code}
120\noindent
121We allow arbitrary binary operators, where the type of the operator
122informs what the types of the arguments must be:
124\begin{code}
125Op : (interpTy a -> interpTy b -> interpTy c) -> Expr G a -> Expr G b ->
126 Expr G c
127\end{code}
129\noindent
130Finally, if expressions make a choice given a boolean. Each branch must
131have the same type:
133\begin{code}
134If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a
135\end{code}
137\noindent
138When we evaluate an \texttt{Expr}, we'll need to know the values in scope, as well as
139their types. \texttt{Env} is an environment, indexed over the types in scope.
140Since an environment is just another form of list, albeit with a strongly specified connection
141to the vector of local variable types, we use the usual \texttt{::} and \texttt{Nil}
142constructors so that we can use the usual list syntax. Given a proof that a variable
143is defined in the context, we can then produce a value from the environment:
145\begin{code}
146data Env : Vect n Ty -> Type where
147 Nil : Env Nil
148 (::) : interpTy a -> Env G -> Env (a :: G)
150lookup : HasType i G t -> Env G -> interpTy t
151lookup stop (x :: xs) = x
152lookup (pop k) (x :: xs) = lookup k xs
153\end{code}
155\begin{code}[caption={Intepreter definition},label=interpdef]
156interp : Env G -> Expr G t -> interpTy t
157interp env (Var i) = lookup i env
158interp env (Val x) = x
159interp env (Lam sc) = \x => interp (x :: env) sc
160interp env (App f s) = interp env f (interp env s)
161interp env (Op op x y) = op (interp env x) (interp env y)
162interp env (If x t e) = if interp env x then interp env t
163 else interp env e
164\end{code}
166\noindent
167Given this, an interpreter (Figure \ref{interpdef})
168is a function which translates an \texttt{Expr} into a
169concrete \Idris{} value with respect to a specific environment:
171\begin{code}
172interp : Env G -> Expr G t -> interpTy t
173\end{code}
175\noindent
176To translate a variable, we simply look it up in the environment:
178\begin{code}
179interp env (Var i) = lookup i env
180\end{code}
182\noindent
183To translate a value, we just return the concrete representation of the value:
185\begin{code}
186interp env (Val x) = x
187\end{code}
189\noindent
190Lambdas are more interesting. In this case, we construct a function which
191interprets the scope of the lambda with a new value in the environment. So, a
192function in the object language is translated to an \Idris{} function:
194\begin{code}
195interp env (Lam sc) = \x => interp (x :: env) sc
196\end{code}
198\noindent
199For an application, we interpret the function and its argument and apply it
200directly. We know that interpreting \texttt{f} must produce a function, because of its
201type:
203\begin{code}
204interp env (App f s) = interp env f (interp env s)
205\end{code}
207\noindent
208Operators and interpreters are, again, direct translations into the equivalent
209\Idris{} constructs. For operators, we apply the function to its operands directly,
210and for \texttt{If}, we apply the \Idris{} \texttt{if...then...else} construct
211directly.
213\begin{code}
214interp env (Op op x y) = op (interp env x) (interp env y)
215interp env (If x t e) = if interp env x then interp env t
216 else interp env e
217\end{code}
219\noindent
220We can make some simple test functions. Firstly, adding two inputs
221\texttt{$\backslash$x. $\backslash$y. y + x} is written as follows:
223\begin{code}
224add : Expr G (TyFun TyInt (TyFun TyInt TyInt))
225add = Lam (Lam (Op (+) (Var stop) (Var (pop stop))))
226\end{code}
228\noindent
229More interestingly, we can write a factorial function. First, we write a \emph{lazy}
230version of the \texttt{App} constructor, so that the recursive branch will only
231be evaluated if necessary:
233\begin{code}
234app : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t
235app = \f, a => App f a
236\end{code}
238\noindent
239The vertical bar annotation before the \texttt{f} argument indicates that this
240argument should be evaluated lazily when \texttt{app} is applied --- that is, the
241argument will be evaluated only when needed.
242Then \texttt{fact}
243(i.e. \texttt{$\backslash$x. if (x == 0) then 1 else (fact (x-1) * x)})
244is written as follows:
246\begin{code}
247fact : Expr G (TyFun TyInt TyInt)
248fact = Lam (If (Op (==) (Var stop) (Val 0))
249 (Val 1) (Op (*) (app fact (Op (-) (Var stop) (Val 1)))
250 (Var stop)))
251\end{code}
253To finish, we write a \texttt{main} program which interprets the factorial function
254on user input:
256\begin{code}
257main : IO ()
258main = do putStr "Enter a number: "
259 x <- getLine
260 print (interp [] fact (cast x))
261\end{code}
263\noindent
264Here, \texttt{cast} is an overloaded function which converts a value from one
265type to another if possible. Here, it converts a string to
266an integer, giving 0 if the input is invalid. An example run of this program
267at the \Idris{} interactive environment is shown in Figure \ref{factrun}.
269\begin{lstlisting}[caption={Running the well-typed interpreter}, label=factrun, escapechar=^]
270$ idris interp.idr
271 ____ __ _
272 / _/___/ /____(_)____
273 / // __ / ___/ / ___/ Version ^\version{}^
274 _/ // /_/ / / / (__ ) http://www.idris-lang.org/
275 /___/\__,_/_/ /_/____/ Type :? for help
277Type checking ./interp.idr
278*interp> :exec
279Enter a number: 6
280720
281*interp>
282\end{lstlisting}
284\subsubsection*{Aside: \texttt{cast}}
286The prelude defines a type class \texttt{Cast} which allows conversion between
287types:
289\begin{code}
290class Cast from to where
291 cast : from -> to
292\end{code}
294\noindent
295It is a \emph{multi-parameter} type class, defining the source type and object
296type of the cast. It must be possible for the type checker to infer \remph{both}
297parameters at the point where the cast is applied.
298There are casts defined between all of the primitive types, as far as
299they make sense.
301\subsection{Unit testing}
303Recall the \texttt{so} data type:
305\begin{code}
306data so : Bool -> Type where
307 oh : so True
308\end{code}
310\noindent
311This requires its parameter to be a \texttt{True} value. One simple application of this
312is to perform unit testing of functions at compile time. For example, we know that
313\texttt{4! = 24} so we can set up a test case as follows:
315\begin{code}
316unitTestFac : so (interp [] fact 4 == 24)
317unitTestFac = oh
318\end{code}
320\noindent
321For the program to compile, the test case must pass. If we change \texttt{24} to \texttt{25},
322say, we will get an error message like the following:
324\begin{lstlisting}
325Type checking ./interp.idr
326interp.idr:64:Can't unify so True with so False
328Specifically:
329 Can't unify True with False
330\end{lstlisting}