StackOverflow2013

Note that there are some explanatory texts on larger screens.

plurals

POImplementing unify algorithm in haskell
text
Body
copied!<p>I am trying to implement a unify function with an algorithm that is specified as</p> <pre><code>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 uniﬁable.” where s1 = unify τ1 τ3 s2 = unify (subst s1 τ2) (subst s1 τ4) </code></pre> <p>with ⊗ being one of the type constructors {→, ×}.</p> <p>However I do not understand how to implement this in haskell. How would I go about this? </p> <pre><code>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 </code></pre>

Querying!

Guidance

An individual column

Larger individual text columns get their own page to allow for proper reading.

SQuiL has stopped working due to an internal error.

If you are curious you may find further information in the browser console, which is accessible through the devtools (F12).

Reload