implementazione dell'algoritmo unificare in Haskell

Question

Sto cercando di implementare una funzione di unificare con un algoritmo che viene specificato come

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 ⊗ essere uno dei costruttori di tipo {→, ×}.

Tuttavia non capisco come implementarlo in haskell. Come andrei su questo?

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 

Questo è un ottimo inizio!

Ora non vi resta che gestire gli altri casi:

Ecco come ci si rappresenti la prima:

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

Si può fare il resto in modo simile utilizzando pattern matching di scomporre il tuo Type nel costruttori e guardie appropriati per gestire casi specifici.

Haskell ha una funzione error :: String -> a che funziona come nel pseudo-codice sopra, e la sintassi if/then/else è la stessa, quindi ci sei quasi!