Type Safe Interpreter for Simple Functional Language in Haskell

gistfile1.txt

This literate Haskell program implements a type safe interpreter for a
simple functional language. Such an interpreter is the "hello world"
example for dependently typed languages and this program mimics it in
Haskell. Generalized algebraic data types and type families are
sufficient.

> {-# LANGUAGE GADTs #-}
> {-# LANGUAGE TypeFamilies #-}
> {-# LANGUAGE TypeOperators #-}
> {-# LANGUAGE MultiParamTypeClasses #-}
>
> module TypeSafeInterpreter where

First, we need natural numbers on the type and value level.

> data Z   = Z
> data S n = S n

We use them to index nested pairs on the type and value level. On the
type level we use a type function defined as associated type synonym
in a type class. On the value level we use overloading via this type
class.

> class Index as n where
>   type as :!: n
>
>   (!) :: as -> n -> as :!: n
>
> instance Index (a,as) Z where
>   type (a,as) :!: Z = a
>
>   (a,_) ! Z = a
>
> instance Index as n => Index (a,as) (S n) where
>   type (a,as) :!: S n = as :!: n
>
>   (_,as) ! S n = as ! n

The expression type is indexed by an environment represented as nested
pairs.

> data Expr :: * -> * -> * where

Variables are represented using de Bruijn indices. The type of the
variable is looked up in the types of environment variables.

>   Var :: Index as n => n -> Expr as (as :!: n)

Primitive values can have any type and work in every environment.

>   Val :: a -> Expr as a

Lambda abstractions extend the environment of the body.

>   Lam :: Expr (a,as) b -> Expr as (a -> b)

Applications do not change the environment but are only type safe if
the argument type of the first expression matches the type of the
second.

>   (:@:) :: Expr as (a -> b) -> Expr as a -> Expr as b

We also support `if then else` expressions.

>   If :: Expr as Bool -> Expr as a -> Expr as a -> Expr as a

For convenience, we can also lift binary operators to do some real
examples later.

>   Op :: (a -> b -> c) -> Expr as a -> Expr as b -> Expr as c

The interpreter evaluates an expression of type `Expr as a` to a
Haskell value of type `a` in the environment of type `as`.

> eval :: Expr as a -> as -> a

The value of a variable is fetched from the environment.

> eval (Var n) as = as ! n

Values evaluate to themselves.

> eval (Val a) _ = a

A lambda abstraction evaluates to a function. The body is evaluated
with an extended environment.

> eval (Lam e) as = \a -> eval e (a,as)

To evaluate an application, the result of evaluating the left argument
(which is known to be a function) is applied to the result of
evaluating the right argument.

> eval (f :@: e) as = eval f as (eval e as)

`if then else` evaluate to the `then` or `else` branch depending on
the condition.

> eval (If b t e) as = if eval b as then eval t as else eval e as

Lifted binary operations are applied to the results of evaluating the
arguments.

> eval (Op op l r) as = op (eval l as) (eval r as)

Now we can evaluate a variable of type `Int` in an environment that
contains an `Int`:

    ghci> eval (Var Z) (42,())
    42

An expression for addition of integers can be defined as follows:

> plus :: Expr as (Int -> Int -> Int)
> plus = Lam (Lam (Op (+) (Var (S Z)) (Var Z)))

Note that de Bruijn indices count the number of lambdas between the
use and introduction of a variable such that this expression
represents `\x.\y.x+y`.

Here is an example application:

    ghci> eval ((plus :@: Val 1) :@: Val 2) ()
    3

We can also define recursive functions like the factorial function.

> fact :: Expr as (Int -> Int)
> fact = Lam (If (Op (==) (Var Z) (Val 0))
>                (Val 1)
>                (Op (*) (Var Z) (fact :@: Op (-) (Var Z) (Val 1))))

Again, as there are no free variables, we call it with an empty
environment `()`.

    ghci> eval (fact :@: Val 4) ()
    24