Реализация алгоритма унификации в haskell - PullRequest
Новая
       26

Реализация алгоритма унификации в haskell

8 голосов
/ 04 октября 2011

Я пытаюсь реализовать функцию унификации с алгоритмом, который указан как 

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

1 Ответ

6 голосов
/ 04 октября 2011 
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 такой же, так что вы почти у цели!

...