typed lambda haskell

import Data.List

main = return ()

main' (ctx,bs) = do
                 line <- getLine
                 putStrLn line
                 main' (ctx,bs)

data Type = Base String | Arr Type Type deriving Eq

instance Show Type where
  show (Base str) = str
  show (Arr t1 t2) = show t1 ++ "->" ++ (show t2)

type Context = [(String, Type)]

addToCtx :: Context ->
            String -> Type ->
            Either String Context
addToCtx [] v t = Right [(v,t)]
addToCtx vs v t = if (v `elem` (map fst vs))
                  then Left $ "Variable " ++ v ++ " is already in context"
                  else Right $ (v,t) : vs

getFromCtx :: Context ->
              String ->
              Either String (String, Type)
getFromCtx [] v = Left $ "Variable " ++ v ++ " is not in context"
getFromCtx (v:vs) v' = if (fst v == v')
                       then Right v
                       else getFromCtx vs v'

data Term = Var String
          | App Term Term
          | Lambda String Term

unlambda :: Term -> ([String], Term)
unlambda (Lambda x l) = (x : vars, rest)
                        where (vars, rest) = unlambda l
unlambda l = ([], l)

instance Show Term where
  show (Var x) = x
  show (App l1 (l@(App l2 l3))) = show l1 ++ " (" ++ (show l) ++ ")"
  show (App l1 l2) = show l1 ++ " " ++ (show l2)
  show (Lambda x l) = "(" ++ "λ" ++ args ++ "." ++ (show body) ++ ")"
                      where (vars, body) = unlambda (Lambda x l)
                            args = concat $ intersperse " " vars

data Expr = VarDecl String Type
          | VarDef String Type Term
          | Print Term
          | Eval Term

unright :: Either a b -> b
unright (Right x) = x

funcMismatch :: Term -> Type -> Type -> String
funcMismatch arg targ tf = "Argument " ++ show arg ++ " : " ++ (show targ)
                           ++ " doesn't match " ++ (show tf)

check :: Context -> Term -> Type -> Either String ()
check ctx
      (Lambda x fx)
      (Arr t1 t2) = check ctx (Var x) t1 >> check ctx fx t2
check _ (Lambda _ _) _ = Left "Lambdas can't have non-arrow types"
check ctx
      term
      t = typeTerm ctx term >>=
                       (\t' -> if t == t'
                              then Right ()
                              else Left $ show term ++ " : " ++ (show t') ++
                                          ", expected " ++ (show t))


typeTerm :: Context -> Term -> Either String Type
typeTerm ctx (Var x) = fmap snd $ getFromCtx ctx x
typeTerm ctx (App f x) = (typeTerm ctx f) >>=
                         (\(Arr t1 t2) -> typeTerm ctx x >>=
                                          (\t -> if t == t1
                                                 then Right t2
                                                 else Left $ "Argument type doesn't match function type"))
typeTerm ctx (Lambda _ _) = Left "Unable to type lambdas"

type Binding = (String, Term)

evalExpr :: Context -> [Binding] -> [String] ->
            Expr ->
            (Context, [Binding], [String])
evalExpr ctx bs ss
         (VarDecl name t) = case addToCtx ctx name t of
                            (Right ctx') -> (ctx',bs,ss)
                            (Left str) -> (ctx,bs,str : ss)
evalExpr ctx bs ss
         (VarDef name t term) = case check ctx term t >>=
                                (\() -> addToCtx ctx name t) of
                                (Right ctx') -> (ctx',(name,term):bs,ss)
                                (Left str) -> (ctx,bs,str : ss)
evalExpr ctx bs ss
         (Print term) = case typeTerm ctx term of
                        (Right t) -> (ctx,bs,(show term ++ " : " ++ (show t)) : ss)
                        (Left str) -> (ctx,bs,str : ss)

evalExprs :: [Expr] -> [String]
evalExprs xs = ext $ foldl (\(c,b,s) e -> evalExpr c b s e) ([],[],[]) xs
               where ext (_,_,s) = reverse s