algoritmo de unificar en Haskell

Question

estoy tratando de implementar una función de unificar con un algoritmo que se especifica como

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) 

con ⊗ ser uno de los constructores de tipo {→, x}.

Sin embargo, no entiendo cómo implementar esto en haskell. ¿Cómo voy a hacer esto?

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 

Answer 1

unify :: Type -> Type -> Substitution 
unify (TVar x) (TVar y) = update (x, TVar y) idSubst 

Este es un gran comienzo!

Ahora sólo tiene que manejar los otros casos:

Aquí te mostramos cómo Representas a la primera de ellas:

unify (TVar x) (TVar y) | x == y = idSubst 

Usted puede hacer el resto de forma similar usando coincidencia de patrones para descomponer su Type en el constructores y guardias apropiados para manejar casos específicos.

Haskell tiene una función error :: String -> a que funciona igual que en su pseudo-código anterior, y la sintaxis if/then/else es la misma, ¡por lo que está casi allí!