Simple Type Inference in Curry

stlc-infer.curry

module typecheck where

data Type = Int | Type ==> Type

data AST
  = Lit Int
  | Var Type String
  | App Type AST AST
  | Lam Type String AST

type Env = [(String, Type)]

infer :: Env -> AST -> (Type, AST)
infer _ (Lit n) = (Int, Lit n)
infer (env ++ [(v,t)] ++ _) (Var t v)
  | not (v `elem` map fst env)
  = (t, (Var t v))
infer env (App t f x)
  | a ==> b =:= fst (infer env f)
  & a       =:= fst (infer env x)
  & t       =:= b
  = (t, App t f x) where a, b free
infer env (Lam t v x)
  | b =:= fst (infer ((v,a):env) x)
  & t =:= (a ==> b)
  = (t, Lam t v x) where a, b free

test :: AST
test = App a (Lam b "y" (Var c "x")) (Var d "x")
  where a, b, c, d free

main :: IO ()
main = do
  let env = [("x", Int), ("f", Int ==> Int)]
  print (snd (infer env test))