在haskell中实现统一算法

Question

我正在尝试使用指定为的算法实现unify函数

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)

⊗是类型构造函数之一{→,×}.

但是我不明白如何在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语法是相同的,所以你几乎就在那里!