--  Andrebbero aggiunti commenti adeguati al codice


data ST =  Var Int | Arrow ST ST
      deriving(Show)


type Substs = ST -> ST 



occur (Var n) (Var m) = (n == m)
occur (Var n) (Arrow t1 t2) = (occur (Var n) t1) || (occur (Var n) t2)
occur t1 t2 = error "First arg of occur must be a variable"


identity x = x


mksubst :: ST -> ST -> Substs
mksubst (Var n) t  (Var m) = if (m == n) then t
                                         else (Var m)
mksubst (Var n) t (Arrow t1 t2) = (Arrow (mksubst (Var n) t t1) (mksubst (Var n) t t2))
mksubst t1 t2 t3 = error "First arg of mksubst must be a variable"


compose f g = \x -> (f (g x))


unify :: ST -> ST -> Substs

 
unify (Var n) t
      | ((Var n) == t)           = identity
      | (not (occur (Var n) t))  = (mksubst (Var n) t)
      | otherwise                = error "Error during type unification!"


unify t (Var n) = (unify (Var n) t)

unify (Arrow t1 t2) (Arrow t3 t4) = let s1 = (unify t1 t3) 
                                        s2 = (unify (s1 t2) (s1 t4))
                                    in (compose s1 s2)

----Altra possibile soluzione


--mancano completamente i commenti al codice --



data TypeVar = TypeVar Int

instance Show TypeVar
   where show (TypeVar n) = "V"++(show n)

instance Eq TypeVar
   where  TypeVar n == TypeVar m = (n == m)



data SimpleType = VarType TypeVar | ArrowType SimpleType SimpleType
   

instance Show SimpleType
   where show (VarType vt) = show vt
         show (ArrowType t1 t2) = "("++(show t1)++" -> "++(show t2)++")"

type TypeSubst = (SimpleType -> SimpleType)




compose f g x = f (g x) 



occur ::  TypeVar -> SimpleType -> Bool

occur tvar1 (VarType tvar2) = tvar1==tvar2

occur tvar (ArrowType type1 type2) = (occur tvar type1) || (occur tvar type2)



pair2TypeSubst :: (TypeVar,SimpleType) -> TypeSubst


pair2TypeSubst (tvar1,tp) (VarType vtype) =  if (vtype == tvar1) 
                                                then tp
                                                else (VarType vtype)

pair2TypeSubst (tvar1,tp) (ArrowType t1 t2) = (ArrowType (pair2TypeSubst (tvar1,tp) t1) (pair2TypeSubst (tvar1,tp) t2))


identity x = x





unifyTypes :: SimpleType -> SimpleType -> TypeSubst


unifyTypes (VarType vtype1) (VarType vtype2) = if (vtype1 == vtype2)
                                                  then identity
                                                  else pair2TypeSubst (vtype1, (VarType vtype2))


unifyTypes (VarType vtype) tp = if (occur vtype tp)
                                    then  error "Not Unifiable Types"
                                    else pair2TypeSubst (vtype,tp)

unifyTypes tp (VarType vtype) = unifyTypes (VarType vtype) tp

unifyTypes (ArrowType t1 t2) (ArrowType t3 t4) = (compose s2 s1)
                                                   where s1 = (unifyTypes t1 t3)
                                                         s2 = unifyTypes (s1 t2) (s1 t4)






--Examples:

myType1 = ArrowType (VarType (TypeVar 1)) (VarType (TypeVar 1))

myType2 = ArrowType 
                   (ArrowType 
                            (VarType (TypeVar 2)) 
                            (VarType (TypeVar 2))
                    ) 
                   (ArrowType 
                            (VarType (TypeVar 3)) 
                            (ArrowType 
                                     (VarType (TypeVar 3)) 
                                     (VarType (TypeVar 2))
                             )
                    )

myType3 = ArrowType (ArrowType (VarType (TypeVar 1)) (VarType (TypeVar 2))) (VarType (TypeVar 1))

myType4 = ArrowType (ArrowType (VarType (TypeVar 3)) (VarType (TypeVar 2))) (VarType (TypeVar 1))


substA = unifyTypes myType1 myType2


substB = unifyTypes myType2 myType4

myType5 = substB myType2 

-- Notice that with our program it is not possible to know that myType1 and myType3 are not unifyable
-- before substB is applyied to an argument