實現在Haskell

Question

統一算法我試圖實現與算法的統一功能被指定爲

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) 

與⊗是所述類型構造{→，×}中的一個。

但我不明白如何在haskell中實現這一點。我將如何去做這件事？

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 

這是一個很好的開始！

現在你只需要處理其他案件：

這裏是你如何代表第一個：

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

您同樣可以使用模式匹配來分解你的Type到做休息適當的建造者和警衛來處理特定的案件。

Haskell有一個error :: String -> a函數，它和上面的僞代碼一樣，而if/then/else語法也是一樣的，所以你幾乎就在那裏！