git.iko.soy/Idris-dev
on f572cd0 help sign in
Idris-dev/docs/tutorial/interp.rst
298 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 an
10``if...then...else`` construct. We will use the dependent type system to
11ensure that any programs which can be represented are well-typed.
13Representing Languages
14----------------------
16First, let us define the types in the language. We have integers,
17booleans, and functions, represented by ``Ty``:
19.. code-block:: idris
21 data Ty = TyInt | TyBool | TyFun Ty Ty
23We can write a function to translate these representations to a concrete
24``Idris`` type — remember that types are first class, so can be
25calculated just like any other value:
27.. code-block:: idris
29 interpTy : Ty -> Type
30 interpTy TyInt = Int
31 interpTy TyBool = Bool
32 interpTy (TyFun A T) = interpTy A -> interpTy T
34We’re going to define a representation of our language in such a way
35that only well-typed programs can be represented. We’ll index the
36representations of expressions by their type and the types of local
37variables (the context), which we’ll be using regularly as an implicit
38argument, so we define everything in a ``using`` block:
40.. code-block:: idris
42 using (G:Vect n Ty)
44The full representation of expressions is given in Listing :ref:`exprty`.
45They 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
52Since expressions are indexed by their type, we can read the typing
53rules of the language from the definitions of the constructors. Let us
54look at each constructor in turn.
56.. _exprty:
57.. code-block:: idris
58 :caption: Expression representation
60 data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where
61 Stop : HasType FZ (t :: G) t
62 Pop : HasType k G t -> HasType (FS k) (u :: G) t
64 data Expr : Vect n Ty -> Ty -> Type where
65 Var : HasType i G t -> Expr G t
66 Val : (x : Int) -> Expr G TyInt
67 Lam : Expr (a :: G) t -> Expr G (TyFun a t)
68 App : Expr G (TyFun a t) -> Expr G a -> Expr G t
69 Op : (interpTy a -> interpTy b -> interpTy c) ->
70 Expr G a -> Expr G b -> Expr G c
71 If : Expr G TyBool ->
72 Lazy (Expr G a) ->
73 Lazy (Expr G a) -> Expr G a
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`` in
78context ``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 the
91``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 de
98Bruijn index of 1, represented as ``Pop Stop``, and ``y 0``, represented
99as ``Stop``. We find these by counting the number of lambdas between the
100definition 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
109``a -> t``, there is a new local variable of type ``a``, which is
110expressed by 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 must
132have the same type, and we will evaluate the branches lazily so that
133only 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, as
146well as their types. ``Env`` is an environment, indexed over the types
147in scope. Since an environment is just another form of list, albeit with
148a strongly specified connection to the vector of local variable types,
149we use the usual ``::`` and ``Nil`` constructors so that we can use the
150usual list syntax. Given a proof that a variable is defined in the
151context, we can then produce a value from the environment:
153.. code-block:: idris
155 data Env : Vect n Ty -> Type where
156 Nil : Env Nil
157 (::) : interpTy a -> Env G -> Env (a :: G)
159 lookup : HasType i G t -> Env G -> interpTy t
160 lookup Stop (x :: xs) = x
161 lookup (Pop k) (x :: xs) = lookup k xs
163.. _interpdef:
164.. code-block:: idris
165 :caption: Intepreter Definition
167 interp : Env G -> Expr G t -> interpTy t
168 interp env (Var i) = lookup i env
169 interp env (Val x) = x
170 interp env (Lam sc) = \x => interp (x :: env) sc
171 interp env (App f s) = interp env f (interp env s)
172 interp env (Op op x y) = op (interp env x) (interp env y)
173 interp env (If x t e) = if interp env x then interp env t
174 else interp env e
176Given this, an interpreter (Listing :ref:`interpdef`) 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
184To translate a variable, we simply look it up in the environment:
186.. code-block:: idris
188 interp env (Var i) = lookup i env
190To translate a value, we just return the concrete representation of the
191value:
193.. code-block:: idris
195 interp env (Val x) = x
197Lambdas are more interesting. In this case, we construct a function
198which interprets the scope of the lambda with a new value in the
199environment. So, a function in the object language is translated to an
200``Idris`` function:
202.. code-block:: idris
204 interp env (Lam sc) = \x => interp (x :: env) sc
206For an application, we interpret the function and its argument and apply
207it directly. We know that interpreting ``f`` must produce a function,
208because of its type:
210.. code-block:: idris
212 interp env (App f s) = interp env f (interp env s)
214Operators and interpreters are, again, direct translations into the
215equivalent ``Idris`` constructs. For operators, we apply the function to
216its operands directly, and for ``If``, we apply the ``Idris``
217``if...then...else`` construct directly.
219.. code-block:: idris
221 interp env (Op op x y) = op (interp env x) (interp env y)
222 interp env (If x t e) = if interp env x then interp env t
223 else interp env e
225Testing
226-------
228We can make some simple test functions. Firstly, adding two inputs
229``\x. \y. y + x`` is written as follows:
231.. code-block:: idris
233 add : Expr G (TyFun TyInt (TyFun TyInt TyInt))
234 add = Lam (Lam (Op (+) (Var Stop) (Var (Pop Stop))))
236More interestingly, a factorial function ``fact``
237(e.g. ``\. if (x == 0) then 1 else (fact (x-1) * x)``),
238can be written as:
240.. code-block:: idris
242 fact : Expr G (TyFun TyInt TyInt)
243 fact = Lam (If (Op (==) (Var Stop) (Val 0))
244 (Val 1)
245 (Op (*) (App fact (Op (-) (Var Stop) (Val 1)))
246 (Var Stop)))
248Running
249-------
251To finish, we write a ``main`` program which interprets the factorial
252function on user input:
254.. code-block:: idris
256 main : IO ()
257 main = do putStr "Enter a number: "
258 x <- getLine
259 print (interp [] fact (cast x))
261Here, ``cast`` is an overloaded function which converts a value from one
262type to another if possible. Here, it converts a string to an integer,
263giving 0 if the input is invalid. An example run of this program at the
264``Idris`` interactive environment is shown in Listing :ref:`factrun`.
266.. _factrun:
267.. code-block:: sh
268 :caption: Running the well-typed interpreter
270 $ idris interp.idr
271 ____ __ _
272 / _/___/ /____(_)____
273 / // __ / ___/ / ___/ Version 0.9.17
274 _/ // /_/ / / / (__ ) http://www.idris-lang.org/
275 /___/\__,_/_/ /_/____/ Type :? for help
277 Type checking ./interp.idr
278 *interp> :exec
279 Enter a number: 6
280 720
281 *interp>
283Aside: ``cast``
284~~~~~~~~~~~~~~~
286The prelude defines a type class ``Cast`` which allows conversion
287between types:
289.. code-block:: idris
291 class Cast from to where
292 cast : from -> to
294It is a *multi-parameter* type class, defining the source type and
295object type of the cast. It must be possible for the type checker to
296infer *both* parameters at the point where the cast is applied. There
297are casts defined between all of the primitive types, as far as they
298make sense.