git.iko.soy/Idris-dev
on cf47310 help sign in
Idris-dev/docs/tutorial/interp.rst
297 lines 9.4 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:
41.. code-block:: idris
43 using (G:Vect n Ty)
45Expressions are indexed by the types of the local variables, and the type of
46the expression itself:
48.. code-block:: idris
50 data Expr : Vect n Ty -> Ty -> Type
52The full representation of expressions is:
54.. code-block:: idris
56 data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where
57 Stop : HasType FZ (t :: G) t
58 Pop : HasType k G t -> HasType (FS k) (u :: G) t
60 data Expr : Vect n Ty -> Ty -> Type where
61 Var : HasType i G t -> Expr G t
62 Val : (x : Int) -> Expr G TyInt
63 Lam : Expr (a :: G) t -> Expr G (TyFun a t)
64 App : Expr G (TyFun a t) -> Expr G a -> Expr G t
65 Op : (interpTy a -> interpTy b -> interpTy c) ->
66 Expr G a -> Expr G b -> Expr G c
67 If : Expr G TyBool ->
68 Lazy (Expr G a) ->
69 Lazy (Expr G a) -> Expr G a
71The code above makes use of the ``Vect`` and ``Fin`` types from the
72Idris standard library. We import them because they are not provided
73in the prelude:
75.. code-block:: idris
77 import Data.Vect
78 import Data.Fin
80Since expressions are indexed by their type, we can read the typing
81rules of the language from the definitions of the constructors. Let us
82look at each constructor in turn.
84We use a nameless representation for variables — they are *de Bruijn
85indexed*. Variables are represented by a proof of their membership in
86the context, ``HasType i G T``, which is a proof that variable ``i``
87in context ``G`` has type ``T``. This is defined as follows:
89.. code-block:: idris
91 data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where
92 Stop : HasType FZ (t :: G) t
93 Pop : HasType k G t -> HasType (FS k) (u :: G) t
95We can treat *Stop* as a proof that the most recently defined variable
96is well-typed, and *Pop n* as a proof that, if the ``n``\ th most
97recently defined variable is well-typed, so is the ``n+1``\ th. In
98practice, this means we use ``Stop`` to refer to the most recently
99defined variable, ``Pop Stop`` to refer to the next, and so on, via
100the ``Var`` constructor:
102.. code-block:: idris
104 Var : HasType i G t -> Expr G t
106So, in an expression ``\x,\y. x y``, the variable ``x`` would have a
107de Bruijn index of 1, represented as ``Pop Stop``, and ``y 0``,
108represented as ``Stop``. We find these by counting the number of
109lambdas between the definition and the use.
111A value carries a concrete representation of an integer:
113.. code-block:: idris
115 Val : (x : Int) -> Expr G TyInt
117A lambda creates a function. In the scope of a function of type ``a ->
118t``, there is a new local variable of type ``a``, which is expressed
119by the context index:
121.. code-block:: idris
123 Lam : Expr (a :: G) t -> Expr G (TyFun a t)
125Function application produces a value of type ``t`` given a function
126from ``a`` to ``t`` and a value of type ``a``:
128.. code-block:: idris
130 App : Expr G (TyFun a t) -> Expr G a -> Expr G t
132We allow arbitrary binary operators, where the type of the operator
133informs what the types of the arguments must be:
135.. code-block:: idris
137 Op : (interpTy a -> interpTy b -> interpTy c) ->
138 Expr G a -> Expr G b -> Expr G c
140Finally, if expressions make a choice given a boolean. Each branch
141must have the same type, and we will evaluate the branches lazily so
142that only the branch which is taken need be evaluated:
144.. code-block:: idris
146 If : Expr G TyBool ->
147 Lazy (Expr G a) ->
148 Lazy (Expr G a) ->
149 Expr G a
151Writing the Interpreter
152=======================
154When we evaluate an ``Expr``, we’ll need to know the values in scope,
155as well as their types. ``Env`` is an environment, indexed over the
156types in scope. Since an environment is just another form of list,
157albeit with a strongly specified connection to the vector of local
158variable types, we use the usual ``::`` and ``Nil`` constructors so
159that we can use the usual list syntax. Given a proof that a variable
160is defined in the context, we can then produce a value from the
161environment:
163.. code-block:: idris
165 data Env : Vect n Ty -> Type where
166 Nil : Env Nil
167 (::) : interpTy a -> Env G -> Env (a :: G)
169 lookup : HasType i G t -> Env G -> interpTy t
170 lookup Stop (x :: xs) = x
171 lookup (Pop k) (x :: xs) = lookup k xs
173Given this, an interpreter is a function which
174translates an ``Expr`` into a concrete Idris value with respect to a
175specific environment:
177.. code-block:: idris
179 interp : Env G -> Expr G t -> interpTy t
181The complete interpreter is defined as follows, for reference. For
182each constructor, we translate it into the corresponding Idris value:
184.. code-block:: idris
186 interp env (Var i) = lookup i env
187 interp env (Val x) = x
188 interp env (Lam sc) = \x => interp (x :: env) sc
189 interp env (App f s) = interp env f (interp env s)
190 interp env (Op op x y) = op (interp env x) (interp env y)
191 interp env (If x t e) = if interp env x then interp env t
192 else interp env e
194Let us look at each case in turn. To translate a variable, we simply look it
195up in the environment:
197.. code-block:: idris
199 interp env (Var i) = lookup i env
201To translate a value, we just return the concrete representation of the
202value:
204.. code-block:: idris
206 interp env (Val x) = x
208Lambdas are more interesting. In this case, we construct a function
209which interprets the scope of the lambda with a new value in the
210environment. So, a function in the object language is translated to an
211Idris function:
213.. code-block:: idris
215 interp env (Lam sc) = \x => interp (x :: env) sc
217For an application, we interpret the function and its argument and apply
218it directly. We know that interpreting ``f`` must produce a function,
219because of its type:
221.. code-block:: idris
223 interp env (App f s) = interp env f (interp env s)
225Operators and conditionals are, again, direct translations into the
226equivalent Idris constructs. For operators, we apply the function to
227its operands directly, and for ``If``, we apply the Idris
228``if...then...else`` construct directly.
230.. code-block:: idris
232 interp env (Op op x y) = op (interp env x) (interp env y)
233 interp env (If x t e) = if interp env x then interp env t
234 else interp env e
236Testing
237=======
239We can make some simple test functions. Firstly, adding two inputs
240``\x. \y. y + x`` is written as follows:
242.. code-block:: idris
244 add : Expr G (TyFun TyInt (TyFun TyInt TyInt))
245 add = Lam (Lam (Op (+) (Var Stop) (Var (Pop Stop))))
247More interestingly, a factorial function ``fact``
248(e.g. ``\x. if (x == 0) then 1 else (fact (x-1) * x)``),
249can be written as:
251.. code-block:: idris
253 fact : Expr G (TyFun TyInt TyInt)
254 fact = Lam (If (Op (==) (Var Stop) (Val 0))
255 (Val 1)
256 (Op (*) (App fact (Op (-) (Var Stop) (Val 1)))
257 (Var Stop)))
259Running
260=======
262To finish, we write a ``main`` program which interprets the factorial
263function on user input:
265.. code-block:: idris
267 main : IO ()
268 main = do putStr "Enter a number: "
269 x <- getLine
270 print (interp [] fact (cast x))
272Here, ``cast`` is an overloaded function which converts a value from
273one type to another if possible. Here, it converts a string to an
274integer, giving 0 if the input is invalid. An example run of this
275program at the Idris interactive environment is:
278.. _factrun:
279.. literalinclude:: ../listing/idris-prompt-interp.txt
282Aside: ``cast``
283---------------
285The prelude defines a type class ``Cast`` which allows conversion
286between types:
288.. code-block:: idris
290 class Cast from to where
291 cast : from -> to
293It is a *multi-parameter* type class, defining the source type and
294object type of the cast. It must be possible for the type checker to
295infer *both* parameters at the point where the cast is applied. There
296are casts defined between all of the primitive types, as far as they
297make sense.