git.iko.soy/Idris-dev
on dae335b help sign in
Idris-dev/docs/tutorial/interp.rst
299 lines 9.5 kB history raw
1.. _sect-interp:
3***********************************
4Example: The Well-Typed Interpreter
5***********************************
7In this section, we’ll use the features we’ve seen so far to write a
8larger example, an interpreter for a simple functional programming
9language, with variables, function application, binary operators and
10an ``if...then...else`` construct. We will use the dependent type
11system to ensure that any programs which can be represented are
12well-typed.
14Representing Languages
15======================
17First, let us define the types in the language. We have integers,
18booleans, and functions, represented by ``Ty``:
20.. code-block:: idris
22 data Ty = TyInt | TyBool | TyFun Ty Ty
24We can write a function to translate these representations to a concrete
25Idris type — remember that types are first class, so can be
26calculated just like any other value:
28.. code-block:: idris
30 interpTy : Ty -> Type
31 interpTy TyInt = Int
32 interpTy TyBool = Bool
33 interpTy (TyFun A T) = interpTy A -> interpTy T
35We’re going to define a representation of our language in such a way
36that only well-typed programs can be represented. We’ll index the
37representations of expressions by their type and the types of local
38variables (the context), which we’ll be using regularly as an implicit
39argument, so we define everything in a ``using`` block (keep in mind
40that everything after this point needs to be indented so as to be
41inside the ``using`` block):
43.. code-block:: idris
45 using (G:Vect n Ty)
47Expressions are indexed by the types of the local variables, and the type of
48the expression itself:
50.. code-block:: idris
52 data Expr : Vect n Ty -> Ty -> Type
54The full representation of expressions is:
56.. code-block:: idris
58 data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where
59 Stop : HasType FZ (t :: G) t
60 Pop : HasType k G t -> HasType (FS k) (u :: G) t
62 data Expr : Vect n Ty -> Ty -> Type where
63 Var : HasType i G t -> Expr G t
64 Val : (x : Int) -> Expr G TyInt
65 Lam : Expr (a :: G) t -> Expr G (TyFun a t)
66 App : Expr G (TyFun a t) -> Expr G a -> Expr G t
67 Op : (interpTy a -> interpTy b -> interpTy c) ->
68 Expr G a -> Expr G b -> Expr G c
69 If : Expr G TyBool ->
70 Lazy (Expr G a) ->
71 Lazy (Expr G a) -> Expr G a
73The code above makes use of the ``Vect`` and ``Fin`` types from the
74Idris standard library. We import them because they are not provided
75in the prelude:
77.. code-block:: idris
79 import Data.Vect
80 import Data.Fin
82Since expressions are indexed by their type, we can read the typing
83rules of the language from the definitions of the constructors. Let us
84look at each constructor in turn.
86We use a nameless representation for variables — they are *de Bruijn
87indexed*. Variables are represented by a proof of their membership in
88the context, ``HasType i G T``, which is a proof that variable ``i``
89in context ``G`` has type ``T``. This is defined as follows:
91.. code-block:: idris
93 data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where
94 Stop : HasType FZ (t :: G) t
95 Pop : HasType k G t -> HasType (FS k) (u :: G) t
97We can treat *Stop* as a proof that the most recently defined variable
98is well-typed, and *Pop n* as a proof that, if the ``n``\ th most
99recently defined variable is well-typed, so is the ``n+1``\ th. In
100practice, this means we use ``Stop`` to refer to the most recently
101defined variable, ``Pop Stop`` to refer to the next, and so on, via
102the ``Var`` constructor:
104.. code-block:: idris
106 Var : HasType i G t -> Expr G t
108So, in an expression ``\x,\y. x y``, the variable ``x`` would have a
109de Bruijn index of 1, represented as ``Pop Stop``, and ``y 0``,
110represented as ``Stop``. We find these by counting the number of
111lambdas between the definition and the use.
113A value carries a concrete representation of an integer:
115.. code-block:: idris
117 Val : (x : Int) -> Expr G TyInt
119A lambda creates a function. In the scope of a function of type ``a ->
120t``, there is a new local variable of type ``a``, which is expressed
121by the context index:
123.. code-block:: idris
125 Lam : Expr (a :: G) t -> Expr G (TyFun a t)
127Function application produces a value of type ``t`` given a function
128from ``a`` to ``t`` and a value of type ``a``:
130.. code-block:: idris
132 App : Expr G (TyFun a t) -> Expr G a -> Expr G t
134We allow arbitrary binary operators, where the type of the operator
135informs what the types of the arguments must be:
137.. code-block:: idris
139 Op : (interpTy a -> interpTy b -> interpTy c) ->
140 Expr G a -> Expr G b -> Expr G c
142Finally, if expressions make a choice given a boolean. Each branch
143must have the same type, and we will evaluate the branches lazily so
144that only the branch which is taken need be evaluated:
146.. code-block:: idris
148 If : Expr G TyBool ->
149 Lazy (Expr G a) ->
150 Lazy (Expr G a) ->
151 Expr G a
153Writing the Interpreter
154=======================
156When we evaluate an ``Expr``, we’ll need to know the values in scope,
157as well as their types. ``Env`` is an environment, indexed over the
158types in scope. Since an environment is just another form of list,
159albeit with a strongly specified connection to the vector of local
160variable types, we use the usual ``::`` and ``Nil`` constructors so
161that we can use the usual list syntax. Given a proof that a variable
162is defined in the context, we can then produce a value from the
163environment:
165.. code-block:: idris
167 data Env : Vect n Ty -> Type where
168 Nil : Env Nil
169 (::) : interpTy a -> Env G -> Env (a :: G)
171 lookup : HasType i G t -> Env G -> interpTy t
172 lookup Stop (x :: xs) = x
173 lookup (Pop k) (x :: xs) = lookup k xs
175Given this, an interpreter is a function which
176translates an ``Expr`` into a concrete Idris value with respect to a
177specific environment:
179.. code-block:: idris
181 interp : Env G -> Expr G t -> interpTy t
183The complete interpreter is defined as follows, for reference. For
184each constructor, we translate it into the corresponding Idris value:
186.. code-block:: idris
188 interp env (Var i) = lookup i env
189 interp env (Val x) = x
190 interp env (Lam sc) = \x => interp (x :: env) sc
191 interp env (App f s) = interp env f (interp env s)
192 interp env (Op op x y) = op (interp env x) (interp env y)
193 interp env (If x t e) = if interp env x then interp env t
194 else interp env e
196Let us look at each case in turn. To translate a variable, we simply look it
197up in the environment:
199.. code-block:: idris
201 interp env (Var i) = lookup i env
203To translate a value, we just return the concrete representation of the
204value:
206.. code-block:: idris
208 interp env (Val x) = x
210Lambdas are more interesting. In this case, we construct a function
211which interprets the scope of the lambda with a new value in the
212environment. So, a function in the object language is translated to an
213Idris function:
215.. code-block:: idris
217 interp env (Lam sc) = \x => interp (x :: env) sc
219For an application, we interpret the function and its argument and apply
220it directly. We know that interpreting ``f`` must produce a function,
221because of its type:
223.. code-block:: idris
225 interp env (App f s) = interp env f (interp env s)
227Operators and conditionals are, again, direct translations into the
228equivalent Idris constructs. For operators, we apply the function to
229its operands directly, and for ``If``, we apply the Idris
230``if...then...else`` construct directly.
232.. code-block:: idris
234 interp env (Op op x y) = op (interp env x) (interp env y)
235 interp env (If x t e) = if interp env x then interp env t
236 else interp env e
238Testing
239=======
241We can make some simple test functions. Firstly, adding two inputs
242``\x. \y. y + x`` is written as follows:
244.. code-block:: idris
246 add : Expr G (TyFun TyInt (TyFun TyInt TyInt))
247 add = Lam (Lam (Op (+) (Var Stop) (Var (Pop Stop))))
249More interestingly, a factorial function ``fact``
250(e.g. ``\x. if (x == 0) then 1 else (fact (x-1) * x)``),
251can be written as:
253.. code-block:: idris
255 fact : Expr G (TyFun TyInt TyInt)
256 fact = Lam (If (Op (==) (Var Stop) (Val 0))
257 (Val 1)
258 (Op (*) (App fact (Op (-) (Var Stop) (Val 1)))
259 (Var Stop)))
261Running
262=======
264To finish, we write a ``main`` program which interprets the factorial
265function on user input:
267.. code-block:: idris
269 main : IO ()
270 main = do putStr "Enter a number: "
271 x <- getLine
272 print (interp [] fact (cast x))
274Here, ``cast`` is an overloaded function which converts a value from
275one type to another if possible. Here, it converts a string to an
276integer, giving 0 if the input is invalid. An example run of this
277program at the Idris interactive environment is:
280.. _factrun:
281.. literalinclude:: ../listing/idris-prompt-interp.txt
284Aside: ``cast``
285---------------
287The prelude defines a type class ``Cast`` which allows conversion
288between types:
290.. code-block:: idris
292 class Cast from to where
293 cast : from -> to
295It is a *multi-parameter* type class, defining the source type and
296object type of the cast. It must be possible for the type checker to
297infer *both* parameters at the point where the cast is applied. There
298are casts defined between all of the primitive types, as far as they
299make sense.