git.iko.soy/Idris-dev
on e32e899 help sign in
Idris-dev/docs/tutorial/interp.rst
288 lines 9.2 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
71Since expressions are indexed by their type, we can read the typing
72rules of the language from the definitions of the constructors. Let us
73look at each constructor in turn.
75We use a nameless representation for variables — they are *de Bruijn
76indexed*. Variables are represented by a proof of their membership in
77the context, ``HasType i G T``, which is a proof that variable ``i``
78in context ``G`` has type ``T``. This is defined as follows:
80.. code-block:: idris
82 data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where
83 Stop : HasType FZ (t :: G) t
84 Pop : HasType k G t -> HasType (FS k) (u :: G) t
86We can treat *Stop* as a proof that the most recently defined variable
87is well-typed, and *Pop n* as a proof that, if the ``n``\ th most
88recently defined variable is well-typed, so is the ``n+1``\ th. In
89practice, this means we use ``Stop`` to refer to the most recently
90defined variable, ``Pop Stop`` to refer to the next, and so on, via
91the ``Var`` constructor:
93.. code-block:: idris
95 Var : HasType i G t -> Expr G t
97So, in an expression ``\x,\y. x y``, the variable ``x`` would have a
98de Bruijn index of 1, represented as ``Pop Stop``, and ``y 0``,
99represented as ``Stop``. We find these by counting the number of
100lambdas between the definition and the use.
102A value carries a concrete representation of an integer:
104.. code-block:: idris
106 Val : (x : Int) -> Expr G TyInt
108A lambda creates a function. In the scope of a function of type ``a ->
109t``, there is a new local variable of type ``a``, which is expressed
110by the context index:
112.. code-block:: idris
114 Lam : Expr (a :: G) t -> Expr G (TyFun a t)
116Function application produces a value of type ``t`` given a function
117from ``a`` to ``t`` and a value of type ``a``:
119.. code-block:: idris
121 App : Expr G (TyFun a t) -> Expr G a -> Expr G t
123We allow arbitrary binary operators, where the type of the operator
124informs what the types of the arguments must be:
126.. code-block:: idris
128 Op : (interpTy a -> interpTy b -> interpTy c) ->
129 Expr G a -> Expr G b -> Expr G c
131Finally, if expressions make a choice given a boolean. Each branch
132must have the same type, and we will evaluate the branches lazily so
133that only the branch which is taken need be evaluated:
135.. code-block:: idris
137 If : Expr G TyBool ->
138 Lazy (Expr G a) ->
139 Lazy (Expr G a) ->
140 Expr G a
142Writing the Interpreter
143=======================
145When we evaluate an ``Expr``, we’ll need to know the values in scope,
146as well as their types. ``Env`` is an environment, indexed over the
147types in scope. Since an environment is just another form of list,
148albeit with a strongly specified connection to the vector of local
149variable types, we use the usual ``::`` and ``Nil`` constructors so
150that we can use the usual list syntax. Given a proof that a variable
151is defined in the context, we can then produce a value from the
152environment:
154.. code-block:: idris
156 data Env : Vect n Ty -> Type where
157 Nil : Env Nil
158 (::) : interpTy a -> Env G -> Env (a :: G)
160 lookup : HasType i G t -> Env G -> interpTy t
161 lookup Stop (x :: xs) = x
162 lookup (Pop k) (x :: xs) = lookup k xs
164Given this, an interpreter is a function which
165translates an ``Expr`` into a concrete Idris value with respect to a
166specific environment:
168.. code-block:: idris
170 interp : Env G -> Expr G t -> interpTy t
172The complete interpreter is defined as follows, for reference. For
173each constructor, we translate it into the corresponding Idris value:
175.. code-block:: idris
177 interp env (Var i) = lookup i env
178 interp env (Val x) = x
179 interp env (Lam sc) = \x => interp (x :: env) sc
180 interp env (App f s) = interp env f (interp env s)
181 interp env (Op op x y) = op (interp env x) (interp env y)
182 interp env (If x t e) = if interp env x then interp env t
183 else interp env e
185Let us look at each case in turn. To translate a variable, we simply look it
186up in the environment:
188.. code-block:: idris
190 interp env (Var i) = lookup i env
192To translate a value, we just return the concrete representation of the
193value:
195.. code-block:: idris
197 interp env (Val x) = x
199Lambdas are more interesting. In this case, we construct a function
200which interprets the scope of the lambda with a new value in the
201environment. So, a function in the object language is translated to an
202Idris function:
204.. code-block:: idris
206 interp env (Lam sc) = \x => interp (x :: env) sc
208For an application, we interpret the function and its argument and apply
209it directly. We know that interpreting ``f`` must produce a function,
210because of its type:
212.. code-block:: idris
214 interp env (App f s) = interp env f (interp env s)
216Operators and interpreters are, again, direct translations into the
217equivalent Idris constructs. For operators, we apply the function to
218its operands directly, and for ``If``, we apply the Idris
219``if...then...else`` construct directly.
221.. code-block:: idris
223 interp env (Op op x y) = op (interp env x) (interp env y)
224 interp env (If x t e) = if interp env x then interp env t
225 else interp env e
227Testing
228=======
230We can make some simple test functions. Firstly, adding two inputs
231``\x. \y. y + x`` is written as follows:
233.. code-block:: idris
235 add : Expr G (TyFun TyInt (TyFun TyInt TyInt))
236 add = Lam (Lam (Op (+) (Var Stop) (Var (Pop Stop))))
238More interestingly, a factorial function ``fact``
239(e.g. ``\. if (x == 0) then 1 else (fact (x-1) * x)``),
240can be written as:
242.. code-block:: idris
244 fact : Expr G (TyFun TyInt TyInt)
245 fact = Lam (If (Op (==) (Var Stop) (Val 0))
246 (Val 1)
247 (Op (*) (App fact (Op (-) (Var Stop) (Val 1)))
248 (Var Stop)))
250Running
251=======
253To finish, we write a ``main`` program which interprets the factorial
254function on user input:
256.. code-block:: idris
258 main : IO ()
259 main = do putStr "Enter a number: "
260 x <- getLine
261 print (interp [] fact (cast x))
263Here, ``cast`` is an overloaded function which converts a value from
264one type to another if possible. Here, it converts a string to an
265integer, giving 0 if the input is invalid. An example run of this
266program at the Idris interactive environment is:
269.. _factrun:
270.. literalinclude:: ../listing/idris-prompt-interp.txt
273Aside: ``cast``
274---------------
276The prelude defines a type class ``Cast`` which allows conversion
277between types:
279.. code-block:: idris
281 class Cast from to where
282 cast : from -> to
284It is a *multi-parameter* type class, defining the source type and
285object type of the cast. It must be possible for the type checker to
286infer *both* parameters at the point where the cast is applied. There
287are casts defined between all of the primitive types, as far as they
288make sense.