1\section{Example: The Well-Typed Interpreter}
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
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
24\begin{SaveVerbatim}{interpty}
29interpTy (TyFun A T) = interpTy A -> interpTy T
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}
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 -> Set
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
64\begin{SaveVerbatim}{exprty}
66data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Set 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 -> Set 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 ->
77 If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a
80\codefig{exprty}{Expression representation}
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 -> Set where
91 stop : HasType fO (t :: G) t
92 pop : HasType k G t -> HasType (fS k) (u :: G) t
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{pop} 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
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.
119A value carries a concrete representation of an integer:
121\begin{SaveVerbatim}{valcon}
123Val : (x : Int) -> Expr G TyInt
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)
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
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 ->
164Finally, if expressions make a choice given a boolean. Each branch must
167\begin{SaveVerbatim}{ifcon}
169If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a
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 -> Set where
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
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
207\codefig{interpdef}{Intepreter definition}
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
222To translate a variable, we simply look it up in the environment:
224\begin{SaveVerbatim}{varinterp}
226interp env (Var i) = lookup i env
232To translate a value, we just return the concrete representation of the value:
234\begin{SaveVerbatim}{valinterp}
236interp env (Val x) = x
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
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
258\begin{SaveVerbatim}{appinterp}
260interp env (App f s) = interp env f (interp env s)
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
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
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))))
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
307(i.e. \texttt{$\backslash$x. if (x == 0) then 1 else (fact (x-1) * x)})
308is written as follows:
310\begin{SaveVerbatim}{facttest}
312fact : Expr G (TyFun TyInt TyInt)
313fact = Lam (If (Op (==) (Var stop) (Val 0))
314 (Val 1) (Op (*) (app fact (Op (-) (Var stop) (Val 1)))
320To finish, we write a \texttt{main} program which interprets the factorial function
323\begin{SaveVerbatim}{factmain}
326main = do putStr "Enter a number: "
328 print (interp [] fact (cast x))
334Here, \texttt{cast} is an overloaded function which converts a value from one
335type to another if possible. Here, it converts a string to
336an integer, giving 0 if the input is invalid. An example run of this program
337at the \Idris{} interactive environment is shown in Figure \ref{factrun}.
339\begin{SaveVerbatim}{factrun}
343 / _/___/ /____(_)____
344 / // __ / ___/ / ___/ Version 0.9.1
345 _/ // /_/ / / / (__ ) http://www.idris-lang.org/
346 /___/\__,_/_/ /_/____/ Type :? for help
348Type checking ./interp.idr
355\codefig{factrun}{Running the well-typed interpreter}
357\subsubsection*{Aside: \texttt{cast}}
359The prelude defines a type class \texttt{Cast} which allows conversion between
362\begin{SaveVerbatim}{castclass}
364class Cast from to where
371It is a \emph{multi-parameter} type class, defining the source type and object
372type of the cast. It must be possible for the type checker to infer \remph{both}
373parameters at the point where the cast is applied.
374There are casts defined between all of the primitive types, as far as
keysesc to close
- j k
- move down, up
- enter
- open
- esc
- back, or up a level
- 1 2 3 4
- readme, files, commits, refs
- /
- filter
- y
- copy the clone command
- c
- compare the chosen commit with another (or shift-click both)
- ?
- show or hide this list