Description

The user is able to use lambda calculator and type inference machine in the context of simple strictly typed lambda calculus.

Type Inference

The task is to be able to derive a type of any given expression, or raise an error if it is impossible. The algorithm return a list of tuples, where each variable has a type.

Examples

Compile the .hs files in type_inference directory:

GHCi> :load environment.hs type_inference.hs
GHCI> import TypeInference

Use cases:

$$x : (x, a), \text{type }b$$

GHCi> let Right pp = principalPair (Var "x") in pp
(Env [("x",TVar "a")],TVar "a")

$$f x : [(f, a \mapsto b), (x, a)], \text{type }b$$

GHCi> let Right pp = principalPair (Var "f" :@ Var "x") in pp
(Env [("f",TVar "a" :-> TVar "b"),("x",TVar "a")],TVar "b")

$$\lambda x.\lambda y.y : [], \text{type }a \mapsto (b \mapsto b)$$

GHCi> let Right pp = principalPair (Lam "x" $ Lam "y" $ Var "y") in pp
(Env [],TVar "a" :-> (TVar "b" :-> TVar "b"))

$$x \mapsto x : \text{No type}$$

GHCi> let Left err = principalPair (Var "x" :@ Var "x") in err
"Can't unify (TVar \"a\") with (TVar \"a\" :-> TVar \"b\")!"

Lambda Calculator

The idea is to be able to compare different expressions. Two expressions are considered equal (beta equivalent) if they could be reduced to the same result. Reductions are independent of the order.

Examples

Compile the .hs files in lambda_calculator directory:

GHCi> :load environment.hs  calculator.hs combinators.hs
GHCI> import Combinators
GHCI> import Main

Use cases:

$$3! = 6$$

GHCI> fac :@ three `betaEq` six
True
GHCI> fac :@ three `betaEq` seven
False