A Type Inference Engine for the Simply Typed Lambda Calculus
by <Your name here>

> module TypedLambdaCalculus (LambdaTerm(..), Type(..), infer)
>  where
> 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


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)

The infer function is the main function you have to write.
You may want to use a helping function that more closely matches the rules,
since you will need to use type environments in the recursion.

> infer :: LambdaTerm -> Maybe Type
> -- you have to fill this in

For testing interactively, you can use the following.

> read_type_print :: IO ()
> read_type_print =
>   do putStr "lambda-typing> "
>      catch (do ln <- getLine
>                print (infer (read ln))
>                read_type_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 ")"

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 (:->))