I am trying to implement a unify function with an algorithm that is specified as
unify α α = idSubst
unify α β = update (α, β) idSubst
unify α (τ1 ⊗ τ2) =
if α ∈ vars(τ1 ⊗ τ2) then
error ”Occurs check failure”
else
update (α, τ1 ⊗ τ2) idSubst
unify (τ1 ⊗ τ2) α = unify α (τ1 ⊗ τ2)
unify (τ1 ⊗1 τ2) (τ3 ⊗2 τ4) = if ⊗1 == ⊗2 then
(subst s2) . s1
else
error ”not unifiable.”
where s1 = unify τ1 τ3
s2 = unify (subst s1 τ2) (subst s1 τ4)
with ⊗ being one of the type constructors {→, ×}.
However I do not understand how to implement this in haskell. How would I go about this?
import Data.List
import Data.Char
data Term = Var String | Abs (String,Term) | Ap Term Term | Pair Term Term | Fst Term | Snd Term
deriving (Eq,Show)
data Op = Arrow | Product deriving (Eq)
data Type = TVar String | BinType Op Type Type
deriving (Eq)
instance Show Type where
show (TVar x) = x
show (BinType Arrow t1 t2) = "(" ++ show t1 ++ " -> " ++ show t2 ++ ")"
show (BinType Product t1 t2) = "(" ++ show t1 ++ " X " ++ show t2 ++ ")"
type Substitution = String -> Type
idSubst :: Substitution
idSubst x = TVar x
update :: (String, Type) -> Substitution -> Substitution
update (x,y) f = (\z -> if z == x then y else f z)
-- vars collects all the variables occuring in a type expression
vars :: Type -> [String]
vars ty = nub (vars' ty)
where vars' (TVar x) = [x]
vars' (BinType op t1 t2) = vars' t1 ++ vars' t2
subst :: Substitution -> Type -> Type
subst s (TVar x) = s x
subst s (BinType op t1 t2) = BinType op (subst s t1) (subst s t2)
unify :: Type -> Type -> Substitution
unify (TVar x) (TVar y) = update (x, TVar y) idSubst
unify :: Type -> Type -> Substitution
unify (TVar x) (TVar y) = update (x, TVar y) idSubst
This is a great start!
Now you just need to handle the other cases:
Here's how you'd represent the first one:
unify (TVar x) (TVar y) | x == y = idSubst
You can do the rest similarly using pattern matching to decompose your Type
into the appropriate constructors and guards to handle specific cases.
Haskell has an error :: String -> a
function that works the same as in your pseudo-code above, and the if/then/else syntax is the same, so you're almost there!
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With