git.iko.soy/Idris-dev
on 5259edc help sign in
Idris-dev/docs/tutorial/interp.rst
300 lines 9.6 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
38local variables (the context). The context can be represented using
39the ``Vect`` data type, and as it will be used regularly it will be
40represented as an implicit argument. To do so we define everything in
41a ``using`` block (keep in mind that everything after this point needs
42to be indented so as to be inside the ``using`` block):
44.. code-block:: idris
46 using (G:Vect n Ty)
48Expressions are indexed by the types of the local variables, and the type of
49the expression itself:
51.. code-block:: idris
53 data Expr : Vect n Ty -> Ty -> Type
55The full representation of expressions is:
57.. code-block:: idris
59 data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where
60 Stop : HasType FZ (t :: G) t
61 Pop : HasType k G t -> HasType (FS k) (u :: G) t
63 data Expr : Vect n Ty -> Ty -> Type where
64 Var : HasType i G t -> Expr G t
65 Val : (x : Int) -> Expr G TyInt
66 Lam : Expr (a :: G) t -> Expr G (TyFun a t)
67 App : Expr G (TyFun a t) -> Expr G a -> Expr G t
68 Op : (interpTy a -> interpTy b -> interpTy c) ->
69 Expr G a -> Expr G b -> Expr G c
70 If : Expr G TyBool ->
71 Lazy (Expr G a) ->
72 Lazy (Expr G a) -> Expr G a
74The code above makes use of the ``Vect`` and ``Fin`` types from the
75Idris standard library. We import them because they are not provided
76in the prelude:
78.. code-block:: idris
80 import Data.Vect
81 import Data.Fin
83Since expressions are indexed by their type, we can read the typing
84rules of the language from the definitions of the constructors. Let us
85look at each constructor in turn.
87We use a nameless representation for variables — they are *de Bruijn
88indexed*. Variables are represented by a proof of their membership in
89the context, ``HasType i G T``, which is a proof that variable ``i``
90in context ``G`` has type ``T``. This is defined as follows:
92.. code-block:: idris
94 data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where
95 Stop : HasType FZ (t :: G) t
96 Pop : HasType k G t -> HasType (FS k) (u :: G) t
98We can treat *Stop* as a proof that the most recently defined variable
99is well-typed, and *Pop n* as a proof that, if the ``n``\ th most
100recently defined variable is well-typed, so is the ``n+1``\ th. In
101practice, this means we use ``Stop`` to refer to the most recently
102defined variable, ``Pop Stop`` to refer to the next, and so on, via
103the ``Var`` constructor:
105.. code-block:: idris
107 Var : HasType i G t -> Expr G t
109So, in an expression ``\x,\y. x y``, the variable ``x`` would have a
110de Bruijn index of 1, represented as ``Pop Stop``, and ``y 0``,
111represented as ``Stop``. We find these by counting the number of
112lambdas between the definition and the use.
114A value carries a concrete representation of an integer:
116.. code-block:: idris
118 Val : (x : Int) -> Expr G TyInt
120A lambda creates a function. In the scope of a function of type ``a ->
121t``, there is a new local variable of type ``a``, which is expressed
122by the context index:
124.. code-block:: idris
126 Lam : Expr (a :: G) t -> Expr G (TyFun a t)
128Function application produces a value of type ``t`` given a function
129from ``a`` to ``t`` and a value of type ``a``:
131.. code-block:: idris
133 App : Expr G (TyFun a t) -> Expr G a -> Expr G t
135We allow arbitrary binary operators, where the type of the operator
136informs what the types of the arguments must be:
138.. code-block:: idris
140 Op : (interpTy a -> interpTy b -> interpTy c) ->
141 Expr G a -> Expr G b -> Expr G c
143Finally, if expressions make a choice given a boolean. Each branch
144must have the same type, and we will evaluate the branches lazily so
145that only the branch which is taken need be evaluated:
147.. code-block:: idris
149 If : Expr G TyBool ->
150 Lazy (Expr G a) ->
151 Lazy (Expr G a) ->
152 Expr G a
154Writing the Interpreter
155=======================
157When we evaluate an ``Expr``, we'll need to know the values in scope,
158as well as their types. ``Env`` is an environment, indexed over the
159types in scope. Since an environment is just another form of list,
160albeit with a strongly specified connection to the vector of local
161variable types, we use the usual ``::`` and ``Nil`` constructors so
162that we can use the usual list syntax. Given a proof that a variable
163is defined in the context, we can then produce a value from the
164environment:
166.. code-block:: idris
168 data Env : Vect n Ty -> Type where
169 Nil : Env Nil
170 (::) : interpTy a -> Env G -> Env (a :: G)
172 lookup : HasType i G t -> Env G -> interpTy t
173 lookup Stop (x :: xs) = x
174 lookup (Pop k) (x :: xs) = lookup k xs
176Given this, an interpreter is a function which
177translates an ``Expr`` into a concrete Idris value with respect to a
178specific environment:
180.. code-block:: idris
182 interp : Env G -> Expr G t -> interpTy t
184The complete interpreter is defined as follows, for reference. For
185each constructor, we translate it into the corresponding Idris value:
187.. code-block:: idris
189 interp env (Var i) = lookup i env
190 interp env (Val x) = x
191 interp env (Lam sc) = \x => interp (x :: env) sc
192 interp env (App f s) = interp env f (interp env s)
193 interp env (Op op x y) = op (interp env x) (interp env y)
194 interp env (If x t e) = if interp env x then interp env t
195 else interp env e
197Let us look at each case in turn. To translate a variable, we simply look it
198up in the environment:
200.. code-block:: idris
202 interp env (Var i) = lookup i env
204To translate a value, we just return the concrete representation of the
205value:
207.. code-block:: idris
209 interp env (Val x) = x
211Lambdas are more interesting. In this case, we construct a function
212which interprets the scope of the lambda with a new value in the
213environment. So, a function in the object language is translated to an
214Idris function:
216.. code-block:: idris
218 interp env (Lam sc) = \x => interp (x :: env) sc
220For an application, we interpret the function and its argument and apply
221it directly. We know that interpreting ``f`` must produce a function,
222because of its type:
224.. code-block:: idris
226 interp env (App f s) = interp env f (interp env s)
228Operators and conditionals are, again, direct translations into the
229equivalent Idris constructs. For operators, we apply the function to
230its operands directly, and for ``If``, we apply the Idris
231``if...then...else`` construct directly.
233.. code-block:: idris
235 interp env (Op op x y) = op (interp env x) (interp env y)
236 interp env (If x t e) = if interp env x then interp env t
237 else interp env e
239Testing
240=======
242We can make some simple test functions. Firstly, adding two inputs
243``\x. \y. y + x`` is written as follows:
245.. code-block:: idris
247 add : Expr G (TyFun TyInt (TyFun TyInt TyInt))
248 add = Lam (Lam (Op (+) (Var Stop) (Var (Pop Stop))))
250More interestingly, a factorial function ``fact``
251(e.g. ``\x. if (x == 0) then 1 else (fact (x-1) * x)``),
252can be written as:
254.. code-block:: idris
256 fact : Expr G (TyFun TyInt TyInt)
257 fact = Lam (If (Op (==) (Var Stop) (Val 0))
258 (Val 1)
259 (Op (*) (App fact (Op (-) (Var Stop) (Val 1)))
260 (Var Stop)))
262Running
263=======
265To finish, we write a ``main`` program which interprets the factorial
266function on user input:
268.. code-block:: idris
270 main : IO ()
271 main = do putStr "Enter a number: "
272 x <- getLine
273 print (interp [] fact (cast x))
275Here, ``cast`` is an overloaded function which converts a value from
276one type to another if possible. Here, it converts a string to an
277integer, giving 0 if the input is invalid. An example run of this
278program at the Idris interactive environment is:
281.. _factrun:
282.. literalinclude:: ../listing/idris-prompt-interp.txt
285Aside: ``cast``
286---------------
288The prelude defines an interface ``Cast`` which allows conversion
289between types:
291.. code-block:: idris
293 interface Cast from to where
294 cast : from -> to
296It is a *multi-parameter* interface, defining the source type and
297object type of the cast. It must be possible for the type checker to
298infer *both* parameters at the point where the cast is applied. There
299are casts defined between all of the primitive types, as far as they
300make sense.