1\section{Example: The Well-Typed Interpreter}
3In this section, we'll use the features we've seen so far to write a larger
4example, an interpreter for a simple functional programming language, with
5variables, function application, binary operators and an \texttt{if...then...else}
6construct. We will use the dependent type system to ensure that any programs
7which can be represented are well-typed. First, let us define the types in the
8language. We have integers, booleans, and functions, represented by \texttt{Ty}:
10\begin{SaveVerbatim}{tydecl}
12data Ty = TyInt | TyBool | TyFun Ty Ty
18We can write a function to translate these representations to a concrete \Idris{}
19type --- remember that types are first class, so can be calculated just like
22\begin{SaveVerbatim}{interpty}
27interpTy (TyFun A T) = interpTy A -> interpTy T
33We're going to define a representation of our language in such a way that only
34well-typed programs can be represented. We'll index the representations of
35expressions by their type and the types of local variables (the context), which
36we'll be using regularly as an implicit argument, so we define everything
37in a \texttt{using} block:
39\begin{SaveVerbatim}{usingg}
47The full representation of expressions is given in Figure \ref{exprty}. They are
48indexed by the types of the local variables, and the type of the expression itself:
50\begin{SaveVerbatim}{exprdecl}
52data Expr : Vect Ty n -> Ty -> Set
58Since expressions are indexed by their type, we can read the typing rules of
59the language from the definitions of the constructors. Let us look at each
62\begin{SaveVerbatim}{exprty}
64data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Set where
65 stop : HasType fO (t :: G) t
66 pop : HasType k G t -> HasType (fS k) (u :: G) t
68data Expr : Vect Ty n -> Ty -> Set where
69 Var : HasType i G t -> Expr G t
70 Val : (x : Int) -> Expr G TyInt
71 Lam : Expr (a :: G) t -> Expr G (TyFun a t)
72 App : Expr G (TyFun a t) -> Expr G a -> Expr G t
73 Op : (interpTy a -> interpTy b -> interpTy c) -> Expr G a -> Expr G b ->
75 If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a
78\codefig{exprty}{Expression representation}
81We use a nameless representation for variables --- they are \emph{de Bruijn indexed}.
82Variables are represented by a proof of their membership in the context,
83\texttt{HasType i G T}, which is a proof that variable \texttt{i} in context
84\texttt{G} has type \texttt{T}. This is defined as follows:
86\begin{SaveVerbatim}{hastype}
88data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Set where
89 stop : HasType fO (t :: G) t
90 pop : HasType k G t -> HasType (fS k) (u :: G) t
96We can treat \remph{stop} as a proof that the most recently defined variable is well-typed,
97and \remph{pop n} as a proof that, if the \texttt{n}th most recently defined variable is
98well-typed, so is the \texttt{n+1}th. In practice, this means we use \texttt{pop} to
99refer to the most recently defined variable, \texttt{pop stop} to refer to the next, and so on,
100via the \texttt{Var} constructor:
102\begin{SaveVerbatim}{varcon}
104Var : HasType i G t -> Expr G t
110So, in an expression \texttt{$\backslash$x. $\backslash$y. x y},
111the variable \texttt{x} would have a de Bruijn index
112of 1, represented as \texttt{pop stop}, and \texttt{y 0}, represented
113as \texttt{stop}. We find these by counting the number of lambdas between the
114definition and the use.
117A value carries a concrete representation of an integer:
119\begin{SaveVerbatim}{valcon}
121Val : (x : Int) -> Expr G TyInt
127A lambda creates a function. In the scope of a function of type \texttt{a -> t}, there is
128a new local variable of type \texttt{a}, which is expressed by the context index:
130\begin{SaveVerbatim}{lamcon}
132Lam : Expr (a :: G) t -> Expr G (TyFun a t)
138Function application produces a value of type \texttt{t} given a function from
139\texttt{a} to \texttt{t}
140and a value of type \texttt{a}:
142\begin{SaveVerbatim}{appcon}
144App : Expr G (TyFun a t) -> Expr G a -> Expr G t
150We allow arbitrary binary operators, where the type of the operator
151informs what the types of the arguments must be:
153\begin{SaveVerbatim}{opcon}
155Op : (interpTy a -> interpTy b -> interpTy c) -> Expr G a -> Expr G b ->
162Finally, if expressions make a choice given a boolean. Each branch must
165\begin{SaveVerbatim}{ifcon}
167If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a
173When we evaluate an \texttt{Expr}, we'll need to know the values in scope, as well as
174their types. \texttt{Env} is an environment, indexed over the types in scope.
175Since an environment is just another form of list, albeit with a strongly specified connection
176to the vector of local variable types, we use the usual \texttt{::} and \texttt{Nil}
177constructors so that we can use the usual list syntax. Given a proof that a variable
178is defined in the context, we can then produce a value from the environment:
180\begin{SaveVerbatim}{envtype}
182data Env : Vect Ty n -> Set where
184 (::) : interpTy a -> Env G -> Env (a :: G)
186lookup : HasType i G t -> Env G -> interpTy t
187lookup stop (x :: xs) = x
188lookup (pop k) (x :: xs) = lookup k xs
193\begin{SaveVerbatim}{interpdef}
195interp : Env G -> Expr G t -> interpTy t
196interp env (Var i) = lookup i env
197interp env (Val x) = x
198interp env (Lam sc) = \x => interp (x :: env) sc
199interp env (App f s) = interp env f (interp env s)
200interp env (Op op x y) = op (interp env x) (interp env y)
201interp env (If x t e) = if interp env x then interp env t
205\codefig{interpdef}{Intepreter definition}
208Given this, an interpreter (Figure \ref{interpdef})
209is a function which translates an \texttt{Expr} into a
210concrete \Idris{} value with respect to a specific environment:
212\begin{SaveVerbatim}{interpty}
214interp : Env G -> Expr G t -> interpTy t
220To translate a variable, we simply look it up in the environment:
222\begin{SaveVerbatim}{varinterp}
224interp env (Var i) = lookup i env
230To translate a value, we just return the concrete representation of the value:
232\begin{SaveVerbatim}{valinterp}
234interp env (Val x) = x
240Lambdas are more interesting. In this case, we construct a function which
241interprets the scope of the lambda with a new value in the environment. So, a
242function in the object language is translated to an \Idris{} function:
244\begin{SaveVerbatim}{laminterp}
246interp env (Lam sc) = \x => interp (x :: env) sc
252For an application, we interpret the function and its argument and apply it
253directly. We know that interpreting \texttt{f} must produce a function, because of its
256\begin{SaveVerbatim}{appinterp}
258interp env (App f s) = interp env f (interp env s)
264Operators and interpreters are, again, direct translations into the equivalent
265\Idris{} constructs. For operators, we apply the function to its operands directly,
266and for \texttt{If}, we apply the \Idris{} \texttt{if...then...else} construct
269\begin{SaveVerbatim}{opinterp}
271interp env (Op op x y) = op (interp env x) (interp env y)
272interp env (If x t e) = if interp env x then interp env t
279We can make some simple test functions. Firstly, adding two inputs
280\texttt{$\backslash$x. $\backslash$y. y + x} is written as follows:
282\begin{SaveVerbatim}{addtest}
284add : Expr G (TyFun TyInt (TyFun TyInt TyInt))
285add = Lam (Lam (Op (+) (Var stop) (Var (pop stop))))
291More interestingly, we can write a factorial function. First, we write a \emph{lazy}
292version of the \texttt{App} constructor, so that the recursive branch will only
293be evaluated if necessary:
295\begin{SaveVerbatim}{lazyapp}
297app : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t
298app = \f, a => App f a
305(i.e. \texttt{$\backslash$x. if (x == 0) then 1 else (fact (x-1) * x)})
306is written as follows:
308\begin{SaveVerbatim}{facttest}
310fact : Expr G (TyFun TyInt TyInt)
311fact = Lam (If (Op (==) (Var stop) (Val 0))
312 (Val 1) (Op (*) (app fact (Op (-) (Var stop) (Val 1)))
318To finish, we write a \texttt{main} program which interprets the factorial function
321\begin{SaveVerbatim}{factmain}
324main = do putStr "Enter a number: "
326 print (interp [] fact (cast x))
332Here, \texttt{cast} is an overloaded function which converts a value from one
333type to another if possible. Here, it converts a string to
334an integer, giving 0 if the input is invalid. An example run of this program
335at the \Idris{} interactive environment is shown in Figure \ref{factrun}.
337\begin{SaveVerbatim}{factrun}
341 / _/___/ /____(_)____
342 / // __ / ___/ / ___/ Version 0.9.1
343 _/ // /_/ / / / (__ ) http://www.idris-lang.org/
344 /___/\__,_/_/ /_/____/ Type :? for help
346Type checking ./interp.idr
353\codefig{factrun}{Running the well-typed interpreter}
355\subsubsection*{Aside: \texttt{cast}}
357The prelude defines a type class \texttt{Cast} which allows conversion between
360\begin{SaveVerbatim}{castclass}
362class Cast from to where
369It is a \emph{multi-parameter} type class, defining the source type and object
370type of the cast. It must be possible for the type checker to infer \remph{both}
371parameters at the point where the cast is applied.
372There 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