.. _sect-interp: ***********************************Example: The Well-Typed Interpreter*********************************** In this section, we’ll use the features we’ve seen so far to write alarger example, an interpreter for a simple functional programminglanguage, with variables, function application, binary operators andan ``if...then...else`` construct. We will use the dependent typesystem to ensure that any programs which can be represented arewell-typed. Representing Languages====================== First, let us define the types in the language. We have integers,booleans, and functions, represented by ``Ty``: .. code-block:: idris     data Ty = TyInt | TyBool | TyFun Ty Ty We can write a function to translate these representations to a concreteIdris type — remember that types are first class, so can becalculated just like any other value: .. code-block:: idris     interpTy : Ty -> Type    interpTy TyInt       = Integer    interpTy TyBool      = Bool    interpTy (TyFun a t) = interpTy a -> interpTy t We're going to define a representation of our language in such a waythat only well-typed programs can be represented. We'll index therepresentations of expressions by their type, **and** the types oflocal variables (the context). The context can be represented usingthe ``Vect`` data type, so we'll need to import ``Data.Vect`` at the top of oursource file: .. code-block:: idris     import Data.Vect Expressions are indexed by the types of the localvariables, and the type of the expression itself: .. code-block:: idris     data Expr : Vect n Ty -> Ty -> Type The full representation of expressions is: .. code-block:: idris     data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where        Stop : HasType FZ (t :: ctxt) t        Pop  : HasType k ctxt t -> HasType (FS k) (u :: ctxt) t     data Expr : Vect n Ty -> Ty -> Type where        Var : HasType i ctxt t -> Expr ctxt t        Val : (x : Integer) -> Expr ctxt TyInt        Lam : Expr (a :: ctxt) t -> Expr ctxt (TyFun a t)        App : Expr ctxt (TyFun a t) -> Expr ctxt a -> Expr ctxt t        Op  : (interpTy a -> interpTy b -> interpTy c) ->              Expr ctxt a -> Expr ctxt b -> Expr ctxt c        If  : Expr ctxt TyBool ->              Lazy (Expr ctxt a) ->              Lazy (Expr ctxt a) -> Expr ctxt a The code above makes use of the ``Vect`` and ``Fin`` types from thebase libraries. ``Fin`` is available as part of ``Data.Vect``. Throughout,``ctxt`` refers to the local variable context. Since expressions are indexed by their type, we can read the typingrules of the language from the definitions of the constructors. Let uslook at each constructor in turn. We use a nameless representation for variables — they are *de Bruijnindexed*. Variables are represented by a proof of their membership inthe context, ``HasType i ctxt T``, which is a proof that variable ``i``in context ``ctxt`` has type ``T``. This is defined as follows: .. code-block:: idris     data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where        Stop : HasType FZ (t :: ctxt) t        Pop  : HasType k ctxt t -> HasType (FS k) (u :: ctxt) t We can treat *Stop* as a proof that the most recently defined variableis well-typed, and *Pop n* as a proof that, if the ``n``\ th mostrecently defined variable is well-typed, so is the ``n+1``\ th. Inpractice, this means we use ``Stop`` to refer to the most recentlydefined variable, ``Pop Stop`` to refer to the next, and so on, viathe ``Var`` constructor: .. code-block:: idris     Var : HasType i ctxt t -> Expr ctxt t So, in an expression ``\x. \y. x y``, the variable ``x`` would have ade Bruijn index of 1, represented as ``Pop Stop``, and ``y 0``,represented as ``Stop``. We find these by counting the number oflambdas between the definition and the use. A value carries a concrete representation of an integer: .. code-block:: idris     Val : (x : Integer) -> Expr ctxt TyInt A lambda creates a function. In the scope of a function of type ``a ->t``, there is a new local variable of type ``a``, which is expressedby the context index: .. code-block:: idris     Lam : Expr (a :: ctxt) t -> Expr ctxt (TyFun a t) Function application produces a value of type ``t`` given a functionfrom ``a`` to ``t`` and a value of type ``a``: .. code-block:: idris     App : Expr ctxt (TyFun a t) -> Expr ctxt a -> Expr ctxt t We allow arbitrary binary operators, where the type of the operatorinforms what the types of the arguments must be: .. code-block:: idris     Op : (interpTy a -> interpTy b -> interpTy c) ->         Expr ctxt a -> Expr ctxt b -> Expr ctxt c Finally, ``If`` expressions make a choice given a boolean. Each branchmust have the same type, and we will evaluate the branches lazily sothat only the branch which is taken need be evaluated: .. code-block:: idris     If : Expr ctxt TyBool ->         Lazy (Expr ctxt a) ->         Lazy (Expr ctxt a) ->         Expr ctxt a Writing the Interpreter======================= When we evaluate an ``Expr``, we'll need to know the values in scope,as well as their types. ``Env`` is an environment, indexed over thetypes in scope. Since an environment is just another form of list,albeit with a strongly specified connection to the vector of localvariable types, we use the usual ``::`` and ``Nil`` constructors sothat we can use the usual list syntax. Given a proof that a variableis defined in the context, we can then produce a value from theenvironment: .. code-block:: idris     data Env : Vect n Ty -> Type where        Nil  : Env Nil        (::) : interpTy a -> Env ctxt -> Env (a :: ctxt)     lookup : HasType i ctxt t -> Env ctxt -> interpTy t    lookup Stop    (x :: xs) = x    lookup (Pop k) (x :: xs) = lookup k xs Given this, an interpreter is a function whichtranslates an ``Expr`` into a concrete Idris value with respect to aspecific environment: .. code-block:: idris     interp : Env ctxt -> Expr ctxt t -> interpTy t The complete interpreter is defined as follows, for reference. Foreach constructor, we translate it into the corresponding Idris value: .. code-block:: idris     interp env (Var i)     = lookup i env    interp env (Val x)     = x    interp env (Lam sc)    = \x => interp (x :: env) sc    interp env (App f s)   = interp env f (interp env s)    interp env (Op op x y) = op (interp env x) (interp env y)    interp env (If x t e)  = if interp env x then interp env t                                             else interp env e Let us look at each case in turn. To translate a variable, we simply look itup in the environment: .. code-block:: idris     interp env (Var i) = lookup i env To translate a value, we just return the concrete representation of thevalue: .. code-block:: idris     interp env (Val x) = x Lambdas are more interesting. In this case, we construct a functionwhich interprets the scope of the lambda with a new value in theenvironment. So, a function in the object language is translated to anIdris function: .. code-block:: idris     interp env (Lam sc) = \x => interp (x :: env) sc For an application, we interpret the function and its argument and applyit directly. We know that interpreting ``f`` must produce a function,because of its type: .. code-block:: idris     interp env (App f s) = interp env f (interp env s) Operators and conditionals are, again, direct translations into theequivalent Idris constructs. For operators, we apply the function toits operands directly, and for ``If``, we apply the Idris``if...then...else`` construct directly. .. code-block:: idris     interp env (Op op x y) = op (interp env x) (interp env y)    interp env (If x t e)  = if interp env x then interp env t                                             else interp env e Testing======= We can make some simple test functions. Firstly, adding two inputs``\x. \y. y + x`` is written as follows: .. code-block:: idris     add : Expr ctxt (TyFun TyInt (TyFun TyInt TyInt))    add = Lam (Lam (Op (+) (Var Stop) (Var (Pop Stop)))) More interestingly, a factorial function ``fact``(e.g. ``\x. if (x == 0) then 1 else (fact (x-1) * x)``),can be written as: .. code-block:: idris     fact : Expr ctxt (TyFun TyInt TyInt)    fact = Lam (If (Op (==) (Var Stop) (Val 0))                   (Val 1)                   (Op (*) (App fact (Op (-) (Var Stop) (Val 1)))                           (Var Stop))) Running======= To finish, we write a ``main`` program which interprets the factorialfunction on user input: .. code-block:: idris     main : IO ()    main = do putStr "Enter a number: "              x <- getLine              printLn (interp [] fact (cast x)) Here, ``cast`` is an overloaded function which converts a value fromone type to another if possible. Here, it converts a string to aninteger, giving 0 if the input is invalid. An example run of thisprogram at the Idris interactive environment is: .. _factrun:.. literalinclude:: ../listing/idris-prompt-interp.txt  Aside: ``cast``--------------- The prelude defines an interface ``Cast`` which allows conversionbetween types: .. code-block:: idris     interface Cast from to where        cast : from -> to It is a *multi-parameter* interface, defining the source type andobject type of the cast. It must be possible for the type checker toinfer *both* parameters at the point where the cast is applied. Thereare casts defined between all of the primitive types, as far as theymake sense.