git.iko.soy/Idris-dev
on 465cc1c help sign in
Idris-dev/docs/tutorial/interp.rst
289 lines 9.3 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)
45The full representation of expressions is given in Listing :ref:`exprty`.
46They are indexed by the types of the local variables, and the type of
47the expression itself:
49.. code-block:: idris
51 data Expr : Vect n Ty -> Ty -> Type
53Since expressions are indexed by their type, we can read the typing
54rules of the language from the definitions of the constructors. Let us
55look at each constructor in turn.
57.. _exprty:
58.. code-block:: idris
59 :caption: Expression representation
61 data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where
62 Stop : HasType FZ (t :: G) t
63 Pop : HasType k G t -> HasType (FS k) (u :: G) t
65 data Expr : Vect n Ty -> Ty -> Type where
66 Var : HasType i G t -> Expr G t
67 Val : (x : Int) -> Expr G TyInt
68 Lam : Expr (a :: G) t -> Expr G (TyFun a t)
69 App : Expr G (TyFun a t) -> Expr G a -> Expr G t
70 Op : (interpTy a -> interpTy b -> interpTy c) ->
71 Expr G a -> Expr G b -> Expr G c
72 If : Expr G TyBool ->
73 Lazy (Expr G a) ->
74 Lazy (Expr G a) -> Expr G a
76We use a nameless representation for variables — they are *de Bruijn
77indexed*. Variables are represented by a proof of their membership in
78the context, ``HasType i G T``, which is a proof that variable ``i``
79in context ``G`` has type ``T``. This is defined as follows:
81.. code-block:: idris
83 data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where
84 Stop : HasType FZ (t :: G) t
85 Pop : HasType k G t -> HasType (FS k) (u :: G) t
87We can treat *Stop* as a proof that the most recently defined variable
88is well-typed, and *Pop n* as a proof that, if the ``n``\ th most
89recently defined variable is well-typed, so is the ``n+1``\ th. In
90practice, this means we use ``Stop`` to refer to the most recently
91defined variable, ``Pop Stop`` to refer to the next, and so on, via
92the ``Var`` constructor:
94.. code-block:: idris
96 Var : HasType i G t -> Expr G t
98So, in an expression ``\x,\y. x y``, the variable ``x`` would have a
99de Bruijn index of 1, represented as ``Pop Stop``, and ``y 0``,
100represented as ``Stop``. We find these by counting the number of
101lambdas between the definition and the use.
103A value carries a concrete representation of an integer:
105.. code-block:: idris
107 Val : (x : Int) -> Expr G TyInt
109A lambda creates a function. In the scope of a function of type ``a ->
110t``, there is a new local variable of type ``a``, which is expressed
111by the context index:
113.. code-block:: idris
115 Lam : Expr (a :: G) t -> Expr G (TyFun a t)
117Function application produces a value of type ``t`` given a function
118from ``a`` to ``t`` and a value of type ``a``:
120.. code-block:: idris
122 App : Expr G (TyFun a t) -> Expr G a -> Expr G t
124We allow arbitrary binary operators, where the type of the operator
125informs what the types of the arguments must be:
127.. code-block:: idris
129 Op : (interpTy a -> interpTy b -> interpTy c) ->
130 Expr G a -> Expr G b -> Expr G c
132Finally, if expressions make a choice given a boolean. Each branch
133must have the same type, and we will evaluate the branches lazily so
134that only the branch which is taken need be evaluated:
136.. code-block:: idris
138 If : Expr G TyBool ->
139 Lazy (Expr G a) ->
140 Lazy (Expr G a) ->
141 Expr G a
143Writing the Interpreter
144-----------------------
146When we evaluate an ``Expr``, we’ll need to know the values in scope,
147as well as their types. ``Env`` is an environment, indexed over the
148types in scope. Since an environment is just another form of list,
149albeit with a strongly specified connection to the vector of local
150variable types, we use the usual ``::`` and ``Nil`` constructors so
151that we can use the usual list syntax. Given a proof that a variable
152is defined in the context, we can then produce a value from the
153environment:
155.. code-block:: idris
157 data Env : Vect n Ty -> Type where
158 Nil : Env Nil
159 (::) : interpTy a -> Env G -> Env (a :: G)
161 lookup : HasType i G t -> Env G -> interpTy t
162 lookup Stop (x :: xs) = x
163 lookup (Pop k) (x :: xs) = lookup k xs
165.. _interpdef:
166.. code-block:: idris
167 :caption: Intepreter Definition
169 interp : Env G -> Expr G t -> interpTy t
170 interp env (Var i) = lookup i env
171 interp env (Val x) = x
172 interp env (Lam sc) = \x => interp (x :: env) sc
173 interp env (App f s) = interp env f (interp env s)
174 interp env (Op op x y) = op (interp env x) (interp env y)
175 interp env (If x t e) = if interp env x then interp env t
176 else interp env e
178Given this, an interpreter (Listing :ref:`interpdef`) is a function which
179translates an ``Expr`` into a concrete Idris value with respect to a
180specific environment:
182.. code-block:: idris
184 interp : Env G -> Expr G t -> interpTy t
186To translate a variable, we simply look it up 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 shown in Listing
267:ref:`factrun`.
270.. literalinclude:: ../listing/idris-prompt-interp.txt
271 :caption: Running the well-typed interpreter
272 :name: factrun
274Aside: ``cast``
275~~~~~~~~~~~~~~~
277The prelude defines a type class ``Cast`` which allows conversion
278between types:
280.. code-block:: idris
282 class Cast from to where
283 cast : from -> to
285It is a *multi-parameter* type class, defining the source type and
286object type of the cast. It must be possible for the type checker to
287infer *both* parameters at the point where the cast is applied. There
288are casts defined between all of the primitive types, as far as they
289make sense.