DOES NOT WORK

> module TypeInfer where
>
> import MonadTransformers
> import StateMTRefs
> import InstsST
> import System(getArgs)


This module contains a type inference algorithm for the simply-typed
lambda calculus ala Curry.

The syntax of types and terms is as follows:

> data Type s = TyVar (TyVarName s) | Type s :-> Type s
> data Term = Var Id | Abs Id Term | App Term Term 

Identifiers are just plain strings.  Type variable names are a little
more complicated.   The reason for this is that the type inference algorithm 
makes use of _unification_.   As a result, variables may be identified
with other types.  This is why we model them as pointers.

> type Id = String
> type TyVarName s = STRef s (Either Id (Type s))

The typing environment is a finite map from term variables to their 
corresponding types.  We model it a list.

> type TyEnv s = [(Id,Type s)]

The type inference monad:

> type TypeInfM s
>   = WithEnv (TyEnv s)     -- typing environment
>   ( WithState [Id]        -- identifier supply
>   ( WithExcept String     -- error detection
>   ( ST s
>   )))

Making a new type variable.

> newTyVar :: TypeInfM s (Type s)
> newTyVar = do
>   x:_ <- updSt tail
>   n <- newRef (Left x)
>   return (TyVar n)


Looking up the type of an identifier.

> -- lookupVar :: Id -> TypeInfM s (Type s)
> lookupVar x = do
>   bindings <- getEnv
>   case lookup x bindings of
>       Nothing -> raise $ "Free variable: " ++ x
>       Just t  -> return t 

> hasType :: Id -> Type s -> TyEnv s -> TyEnv s
> (x `hasType` t) bindings = (x,t) : bindings

> typeOf :: Term -> TypeInfM s (Type s)
> typeOf (Var x) = lookupVar x 
> typeOf (Abs x e) = do
>   t  <- newTyVar
>   t' <- inModEnv (x `hasType` t) (typeOf e) 
>   return (t :-> t')
> typeOf (App e1 e2) = do
>   t  <- typeOf e1
>   t' <- typeOf e2
>   x  <- newTyVar 
>   unify t (t' :-> x)
>   return x


> unify :: Type s -> Type s -> TypeInfM s ()
> unify (TyVar x) t = x |-> t
> unify t (TyVar x) = x |-> t
> unify (s :-> s') (t :-> t') = unify s t >> unify s' t'


> (|->) :: TyVarName s -> Type s -> TypeInfM s ()
> x |-> t = follow t >>= bindTo
>   where
>   bindTo (TyVar y)
>       | x == y = return ()
>   bindTo t = do
>       occurs <- x `occursIn` t
>       if occurs then raise "Occurs check!" 
>                 else writeRef x (Right t)

> follow it@(TyVar x) = readRef x >>= either (const (return it)) follow
> follow it = return it

> occursIn :: TyVarName s -> Type s -> TypeInfM s Bool
> x `occursIn` t = do
>   t' <- follow t
>   case t' of
>       TyVar y -> return (x == y)
>       a :-> b -> do
>           inA <- x `occursIn` a
>           inB <- x `occursIn` b
>           return (inA || inB)


-- tests ---------------------------------------------------------------------

> test :: Term -> Either String String
> test t = runST
>   ( removeExcept
>   $ removeState_ names 
>   $ removeEnv []
>   $ typeOf t >>= showType      
>   )

> showType it = do
>   t <- follow it 
>   case t of
>       TyVar x -> do Left x <- readRef x; return x
>       a :-> b -> do
>           a' <- showType a
>           b' <- showType b
>           return $ "(" ++ a' ++ ") -> (" ++ b' ++ ")"

> names :: [Id]
> names = concat [ map (:d) ['a'..'z'] | d <- ["", "'"] ++ map show [1..] ]

> tId = Abs "x" $ Var "x"
> tK  = Abs "x" $ Abs "y" $ Var "x"
> tApp = Abs "f" $ Abs "x" $ App (Var "f") (Var "x")
> tS  = Abs "f" $ Abs "g" $ Abs "x" $ App (App (Var "f") (Var "x"))
>                                         (App (Var "g") (Var "x"))
> tSApp = Abs "x" $ App (Var "x" ) (Var "x")
> tO    = App tSApp tSApp

> tests = [tId, tK, tApp, tS, tSApp, tO]

> main = getArgs >>= putStrLn . show . test . (tests !!) . read . head