The Full Type Frame model of the Simply Typed Lambda Calculus
(see Carl Gunter, Semantics of Programming Languages, MIT Press, 1993)
translated into Haskell by Gary T. Leavens

> module SimplyTypedModel (LambdaTerm(..), Type(..), meaning)
>  where
> import List hiding (find)
> import ParserFunctions
> import LexerTools
> infixr 0 :->

Abstract Syntax for simply typed lambda terms and their types

> type Var = String
> data LambdaTerm = Varref Var
>             | Lambda Var Type LambdaTerm
>             | App LambdaTerm LambdaTerm
>               deriving Eq

> data Type = O | Type :-> Type
>             deriving Eq

> data Value = Nat Integer | Fun (Value -> Value)

Type environments are association lists.
Note that, unlike the formalism, the overriding bindings are
at the front of the list.

> type TypeEnv = [Binding]
> type Binding = (Var, Type)

Similarly, (value) environments are association lists.

> type Env = [ValBinding]
> type ValBinding = (Var, Value)

Functions on environments

> find :: [(Var,a)] -> Var -> a
> find [] x     = error ("variable `" ++ x ++ "' is not bound")
> find ((y,a):bs) x = if y == x then a else find bs x

> bind :: Var -> a -> [(Var,a)]
> bind y a = [(y,a)]

> dom :: [(a, b)] -> [a]
> dom = map fst

> overlay :: [(Var,a)] -> [(Var,a)] -> [(Var,a)]
> overlay env1 env2 =
>                 env1 ++ [(y,a) | (y,a) <- env2, not (y `elem` (dom env1))]

The initial (value) environment.  To make examples easier, we have some
built-in values.

> initialEnv :: Env
> initialEnv = [("zero", Nat 0), ("one", Nat 1), ("two", Nat 2), ("three", Nat 3),
>               ("x", Nat 24), ("y", Nat 25), ("z", Nat 26)]

The meaning function

> meaning :: LambdaTerm -> Value
> meaning e = eval e initialEnv

The eval function gives the meaning of a term in an environment.
Note that eval e eta is like [[H |> e : t]](eta),
except we are ignoring H and t. 

> eval :: LambdaTerm -> Env -> Value
> eval (Varref x) eta = find eta x
> eval (App e e') eta = 
>      case (eval e eta) of
>         (Fun f) -> f (eval e' eta)
>         v -> error ("attempt to apply a non-function" ++ show v)
> eval (Lambda x _ e) eta = (Fun f)
>       where f y = eval e eta'
>                   where eta' = overlay (bind x y) eta

For testing interactively, you can use the following.

> read_eval_print :: IO ()
> read_eval_print =
>   do putStr "lambda-term? "
>      catch (do ln <- getLine
>                print (meaning (read ln))
>                read_eval_print)
>            (\e -> fail (show e))

The show function can be used to output terms in a nice fashion.

> instance Show LambdaTerm where
>    showsPrec p (Varref x) = showString x
>    showsPrec p (Lambda x t body) = 
>          showString "(\\" . showString x . showString ": "
>                         . showsPrec p t . showString " . "
>                         . showsPrec p body . showString ")"
>    showsPrec p (App t1 t2) =
>          showString "(" . showsPrec p t1 . showString " "
>                         . showsPrec p t2 . showString ")"

> instance Show Type where
>    showsPrec p O = showString "o"
>    showsPrec p (t1 :-> t2) = 
>          showString "(" . showsPrec p t1 . showString " -> "
>                         . showsPrec p t2 . showString ")"

> instance Show Value where
>    showsPrec p (Nat i) = showsPrec p i
>    showsPrec p (Fun f) = showString "<function>"

Parsing functions are below.  These are based on the ParsingFunctions
and LexerTools modules.


The following Read instance puts the parts of the parser together.

> instance Read LambdaTerm where
>    readsPrec n input =
>        let parses = lambdaParser (lambdaScanner input)
>        in case parses of
>             [(lt,[])] -> [(lt,[])]
>             _ -> []

The scanner needs definitions of keywords (reserved really)
and special symbols.

> lambdaScanner :: [Char] -> [Token]
> lambdaScanner = scanning lambdaKeywords lambdaSymbols []
>    where lambdaKeywords = ["o"]
>          lambdaSymbols = ["(",  "\\", ":", ".", ")", "->"]

The input grammar is fully parenthesized.  This isn't nice for uses,
but simplifies the parsing.

> lambdaParser = expr
>  where expr =
>                p_Id                             `using` Varref
>             $| (p_check "(" /$~ expr
>                             $~ expr
>                             $~/ p_check ")")    `using` (uncurry App)
>             $| (((p_check "(" /$~ p_check "\\"
>                              /$~ p_Id)
>                  $~ (p_check ":" /$~ typeexp))
>                  $~ (p_check "." /$~ expr
>                             $~/ p_check ")"))
>                                            `using` (uncurry (uncurry Lambda))
>        typeexp =
>                 (p_check "o")                  `p_return` O
>             $| ((p_check "(" /$~ typeexp)
>                 $~ (p_check "->" /$~ typeexp
>                       $~/ p_check ")"))        `using` (uncurry (:->))