A toy interpreter for a simple imperative language using GADTs and monad transformers.

L1.lhs

Haskell L1 Interpreter
======================

This is a simple interpreter for L1, with two little twists: It uses
monad transformers to represent state and erroneous computations, and
generalised algebraic datatypes (GADTs) for implicit type checking.

Extensions and Imports
----------------------

We represent expressions using GADTs and a kind signature, both of which
are extensions to the Glasgow Haskell Compiler (GHC). These need to be
turned on explicitely.

> {-# LANGUAGE GADTs, KindSignatures #-}

> module Semantics.L1 (Expr, Store, Eval, eval, runEval) where

To avoid Prelude.lookup and Data.Map.lookup clashing, we simply hide
Prelude.lookup since it is not used in this module.

> import Prelude hiding (lookup)

Our Eval monad is based on the Identity monad. We then wrap it in a
StateT monad transformer which gives us a nice way of dealing with the
store. This is then wrapped again in an ErrorT transformer to give us
error handling support.

> import Control.Monad (liftM2)
> import Control.Monad.Error (ErrorT, runErrorT, throwError)
> import Control.Monad.Identity (Identity, runIdentity)
> import Control.Monad.State (StateT, runStateT, gets, modify)

The store is represented as a Data.Map, so we include the appropriate
type constructor and functions as well.

> import Data.Map (Map, empty, insert, lookup, member, singleton)

Intref and the store
--------------------

For simplicity, we refer to locations via strings.

> type Intref = String

Our store is represented as a map with Intref as the key type and values
of type Integer (Note: That's Integer, not Int, so we're closer to
actually representing integers since Integer can be almost arbitrarily
large.)

> type Store = Map Intref Integer

Expressions as a GADT
---------------------

The expression syntax is:

  e  ::= skip | n | b | e1 op e2 | l := e | !l | e1 ; e2 |
         if e1 then e2 else e3 | while e1 do e2
  op ::= + | >=

We can expand the e1 op e2 case into e1 + e2 and e1 >= e2 and annotate
the entire expression syntax with types (here, T represents an arbitrary
expression type, i.e. T ::= Integer | Bool | Unit) to include the
typing rules:

  e ::= skip::Unit | n::Integer | b::Bool |
        ((e1::Integer) + (e2::Integer))::Integer |
        ((e1::Integer) >= (e2::Integer))::Bool |
        ((l::Intref) := (e::Integer))::Unit |
        (!(l::Intref))::Integer | ((e1::Unit) ; (e2::T))::T |
        (if (e1::Bool) then (e2::T) else (e3::T))::T |
        (while (e1::Bool) do (e2::Unit))::Unit

The point here is that the typing rules are syntax-directed, and that
the annotated expression syntax covers all typing rules. This means that
if we can make the annotations part of our expression type (in Haskell),
we can get rid of static type checking entirely: Haskell will take care
of it for us.

And that's where generalised algebraic datatypes come in: If we make
Expr, the type constructor representing expressions, a GADT, then we can
translate our annotated expression syntax directly into type
expressions.

An example: The assignment syntax is

  ((l::Intref) := (e::Integer))::Unit

and we can translate it into the following type expression (note that ()
is Haskell's Unit type):

   EAssign :: Intref -> Expr Integer -> Expr ()

We proceed in a similar way by mapping each syntax rule into a GADT type
constructor to produce Expr:

> data Expr :: * -> * where
>   ESkip   :: Expr ()
>   EInt    :: Integer -> Expr Integer
>   EBool   :: Bool -> Expr Bool
>   EPlus   :: Expr Integer -> Expr Integer -> Expr Integer
>   EGTEQ   :: Expr Integer -> Expr Integer -> Expr Bool
>   EAssign :: Intref -> Expr Integer -> Expr ()
>   EDeref  :: Intref -> Expr Integer
>   ESeq    :: Expr () -> Expr a -> Expr a
>   EIf     :: Expr Bool -> Expr a -> Expr a -> Expr a
>   EWhile  :: Expr Bool -> Expr () -> Expr ()

Monadic Evaluation
------------------

We compose the Identity monad with the StateT and the ErrorT monad
transformers to produce the Eval monad in which the expression is
evaluated. The type of the state is Store, and the errors are
represented as Strings.

> type Eval a = ErrorT String (StateT Store Identity) a

runEval st ev runs the evaluation action ev in store st.

> runEval :: Store -> Eval a -> (Either String a, Store)
> runEval st ev = runIdentity (runStateT (runErrorT ev) st)

The evaluation function eval itself takes an expression and returns its
value in the Eval monad.

> eval                :: Expr a -> Eval a
> eval ESkip          = return ()
> eval (EInt n)       = return n
> eval (EBool b)      = return b
> eval (EPlus e1 e2)  = liftM2 (+)  (eval e1) (eval e2)
> eval (EGTEQ e1 e2)  = liftM2 (>=) (eval e1) (eval e2)
> eval (EIf e1 e2 e3) = do cond <- eval e1
>                          if cond then eval e2 else eval e3
> eval (EAssign r e)  = do n <- eval e
>                          isMember <- gets $ member r
>                          if isMember then modify $ insert r n
>                                      else throwError assignErrorMsg
> eval (EDeref r)     = do val <- gets $ lookup r
>                          case val of
>                            Just x  -> return x
>                            Nothing -> throwError derefErrorMsg
> eval (ESeq e1 e2)   = eval e1 >> eval e2
> eval (EWhile e1 e2) = eval $ EIf e1 (ESeq e2 (EWhile e1 e2)) ESkip

> assignErrorMsg :: String
> assignErrorMsg = "cannot assign to previously unbound location"

> derefErrorMsg :: String
> derefErrorMsg = "cannot derefence unbound location"

Examples
--------

> ex0 :: (Expr Integer, Store)
> ex0 = (EInt 0, empty)

> ex1 :: (Expr Integer, Store)
> ex1 = (EIf (EBool True) (EInt 1) (EInt 0), empty)

> ex2 :: (Expr Integer, Store)
> ex2 = (ESeq (EAssign "l" (EInt 2)) (EDeref "l"), singleton "l" 1)

> ex2a :: (Expr Integer, Store)
> ex2a = (ESeq (EAssign "l" (EInt 1)) (EDeref "l"), empty)

The following should throw an error: "l" is an unbound location in ex2b.

> ex2b :: (Expr Integer, Store)
> ex2b = (EDeref "l", empty)

> ex3 :: (Expr Bool, Store)
> ex3 = ( EGTEQ (ESeq (EAssign "l" (EInt 2)) (EDeref "l"))
>               (ESeq (EAssign "l" (EInt 1)) (EDeref "l"))
>       , singleton "l" 5
>       )