Tiago Cogumbreiro

data Type = UnitType | TypeVar String | ArrowType Type Type

-- Pretty print types

instance Show Type where show UnitType = "Unit" show (TypeVar x) = x
    show (ArrowType t1 t2) = "(" ++ (show t1) ++ " -> " ++ (show t2)
    ++ ")"

-- Expressions

data Expr = Unit | Var String | App Expr Expr | Fun String Expr

type TypeAssign = (String, Type)

type TypeEnv = [TypeAssign]

-- pretty print values

instance Show Expr where show Unit = "unit" show (Var x) = x show (App
    e1 e2) = "(" ++ (show e1) ++ " " ++ (show e2) ++ ")" show (Fun x
    e) = "(fun " ++ x ++ " = " ++ (show e) ++ ")"

env_lookup:: TypeEnv -> String -> Type

env_lookup ((x,t):xs) y | x == y = t | otherwise = (env_lookup xs y)

env_lookup [] x = error ("Key `" ++ x ++ "' not found.")

-- Functions to generate fresh type-variables:

numsFrom n = n : numsFrom (n + 1)

naturals = numsFrom 1

listOf x = x : listOf x

strNaturals = map show naturals

genNames name = map (uncurry (++)) (zip (listOf name) strNaturals)

genTypeVars name = map (\ x -> TypeVar x) (genNames name)

-- The result type

data Constraint = Eq Type Type

-- Make it print'able instance Show Constraint where show (Eq t1 t2) =
(show t1) ++ "=" ++ (show t2)

-- The algorithm to infer types

infer:: TypeEnv -> Expr -> Type -> [Type] -> [Constraint]

infer _ Unit t vars = [Eq t UnitType]

infer type_env (Var x) t vars = [(Eq ret_type t)] where ret_type =
    env_lookup type_env x

infer type_env (App m n) t (a:vars) = e1_result ++ e2_result where
    e2_result = infer type_env n a vars new_name = (show a) ++ "_"
    new_vars = genTypeVars new_name e1_result = infer type_env m
    (ArrowType a t) new_vars

infer type_env (Fun x m) t (a:b:vars) = (Eq t (ArrowType a
    b)):exp_result where exp_result = infer ((x,a):type_env) m b vars

-- Generates the constraints for certain type inferTypes type_env exp
= infer type_env exp a vars where a = head (genTypeVars "a") vars =
tail (genTypeVars "a")