An implementation of the type unification algorithm [1], using simple types. Used the explanation in this week's Comparative Programming lecture as reference.

unification.hs

import qualified Data.Maybe as M
import Debug.Trace

-- Type type
data Type =  Val Char | Arrow Type Type deriving Eq
instance Show Type where
	show (Val c) = [c]
	show (Arrow t1 t2) = "(" ++ (show t1) ++ " -> " ++ (show t2) ++ ")"

-- Substitution type
data Substitution = Id | Subst Type Type
instance Show Substitution where
	show Id = "Id"
	show (Subst t1 t2) = "[" ++ (show t1) ++ " / " ++ (show t2) ++ "]"

-- Applies a substitution rule to a type
substitute :: Substitution -> Type -> Type
substitute Id t = t
substitute (Subst e1 e2) (Val c) = if (Val c) == e2 then e1 else (Val c)
substitute (Subst e1 e2) (Arrow a1 a2)
	| (Arrow a1 a2) == e2 = e1 -- substitute whole exp
	| otherwise           = Arrow lhs rhs where -- keep the arrow, substitute its children
		lhs = substitute (Subst e1 e2) a1 
		rhs = substitute (Subst e1 e2) a2

-- Combines two substitutions into one
combineSubsts :: Substitution -> Substitution -> Substitution
combineSubsts sub Id = sub
combineSubsts sub (Subst e21 e22) = Subst lhs rhs where
	lhs = substitute sub e21
	rhs = substitute sub e22

-- Returns True if the first arg occurs somewhere in the second arg
occursIn :: Type -> Type -> Bool
occursIn (Val v1) (Val v2) = v1 == v2
occursIn (Arrow _ _) (Val _) = False -- an arrow cannot be found inside a var!
occursIn s (Arrow a1 a2) = s == (Arrow a1 a2) || occursIn s a1 || occursIn s a2 -- explore the branches

-- Returns the disagreement set (either an empty list or a single item)
disagree :: Type -> Type -> [(Type, Type)]
disagree (Arrow a1 a2) (Arrow b1 b2) = if length lhs > 0 then lhs else rhs where
	lhs = disagree a1 b1
	rhs = disagree a2 b2
disagree t1 t2 = if t1 == t2 then [] else [(t1,t2)]

-- Yay! The Unification algorithm
unify :: Type -> Type -> Maybe Substitution
unify t1 t2 = iter Id t1 t2

iter :: Substitution -> Type -> Type -> Maybe Substitution
iter v t1 t2
	| (substitute v t1) == (substitute v t2) = Just v -- substitution found!
	| not (occursIn (fst d) (snd d)) = iter (combineSubsts (Subst (snd d) (fst d)) v) t1 t2 -- a does not occur in b
	| not (occursIn (snd d) (fst d)) = iter (combineSubsts (Subst (fst d) (snd d)) v) t1 t2 -- b does not occur in a
	| otherwise        = Nothing
	where
		dS = disagree (substitute v t1) (substitute v t2)
		d = head dS

-- Test types
a = Arrow (Val 'a') (Val 'a')
b = Arrow (Arrow (Val 'b') (Val 'b')) (Arrow (Val 'b') (Val 'b'))