-- STLC type inference in 8 lines of Curry

data Ty = Iota | Arr Ty Ty
data Tm = Var String | App Tm Tm | Lam String Tm
infer ctx (Var x) = case lookup x ctx of 
                     Just t -> t
                     Nothing -> error (x ++ " undefined")
infer ctx (App e1 e2) | infer ctx e2 `Arr` t =:= infer ctx e1 
                      = t where t free
infer ctx (Lam x e)   = t `Arr` infer ((x,t):ctx) e where t free


x = Var "x"
y = Var "y"
z = Var "z"

tm_id = Lam "x" x
tm_S = Lam "x" $ Lam "y" $ Lam "z" $ App (App x z) (App y z)
tm_bad = Lam "x" $ App x x

ty_id = infer [] tm_id
ty_S = infer [] tm_S
ty_bad = infer [] tm_bad

main =
       -- ty_id
       ty_S
       -- ty_bad