haskell - 使用 Data.Comp.Unification 在 Haskell 中找到最通用的统一器(初学者问题)

Question

我在 haskell 中有以下结构，它实现了一些打印机制并调用了统一器。我从 main 得到以下错误:

0 =/= int

似乎认为0是一个数字而不是一个变量。以下是完整的实现。

 data CType 
      = CVar Int 
      | CArr CType CType
      | CInt
      | CBool
      deriving (Eq, Data)

data Constraint 
  = Equality CType CType
    deriving (Eq, Data)

我有一些基本类型(int 和 bool)、箭头类型和类型变量。然后我运行一些生成等式约束的算法，这些等式约束以上述方式表示。

我的目标是给定一个约束列表，我想找到最通用的统一器。

我遇到了这个图书馆:http://hackage.haskell.org/package/compdata-0.1/docs/Data-Comp-Unification.html

由于我是 Haskell 的新手，我无法立即弄清楚是否可以直接应用它。我可以使用这个库还是建议我从头开始编写统一器？

更新

我目前正在对代码进行以下更改，但遇到方程式的统一错误

f=g

module SolveEq where
import Data.Data
import Data.Void
import Data.List as List
import Data.Map as Map
import Data.Set as Set
import Data.Maybe (fromJust)
import Data.Maybe (isJust)
import Control.Monad
import TypeCheck
import Data.Comp.Variables
import Data.Comp.Unification
import Data.Comp.Term
import Data.Comp.Derive
import Constraint
import Lang

data CTypeF a 
    = CVarF Int 
    | CArrF a a
    | CIntF
    | CBoolF
    deriving (Data, Functor, Foldable, Traversable, Show, Eq)

$(makeShowF ''CTypeF)


example :: String
example = showF (CIntF :: CTypeF String)

instance HasVars CTypeF Int where
isVar (CVarF x) = Just x
isVar (CArrF x y) = Nothing
isVar CIntF = Nothing
isVar CBoolF = Nothing

type CType_ = Term CTypeF

f :: CType_
f = Term (CVarF 0)

g :: CType_
g = Term CIntF


unravel :: CType_ -> CType
unravel a = 
    case unTerm a of 
        CVarF i -> CVar i
        CArrF a b -> CArr (unravel a) (unravel b)
        CIntF -> CInt
        CBoolF -> CBool

getUnify :: Either (UnifError CTypeF Int) (Subst CTypeF Int)
getUnify = unify [(f,g)]

main = case getUnify of
  Left (FailedOccursCheck v term)     -> putStrLn ("failed occurs check " ++ show v ++ ": " ++ (show $ unravel term))
  Left (HeadSymbolMismatch t1 t2)     -> putStrLn ("head symbol mismatch " ++ show (unravel t1)  ++ " =/= " ++ (show $ unravel t2))
  Left (UnifError str)     -> putStrLn str
  Right (subst :: Subst CTypeF Int) -> print (fmap unravel subst)

问题出在 unify [(f,g)] 中，我希望将 0 映射到 Int。但是好像看不出0是一个变量。我的 isVar 可能有问题吗？

注意:我运行的是 compdata-0.12

Answer 1

我相信您可以使用该库，但您必须对数据结构进行微小的更改。具体来说，您必须将其重写为签名仿函数而不是递归数据类型。

这是什么意思:您的 CType 类型是递归的，因为它在其构造函数之一 (CArr) 中包含 CType 的其他实例。将递归数据类型重写为签名意味着创建一个采用类型参数的数据类型，并在任何需要使用递归的地方使用该类型参数。像这样:

 data CTypeF a 
      = CVar Int 
      | CArr a a
      | CInt
      | CBool
      deriving (Eq, Data)

现在，在您之前传递 CType 的程序中，您需要处理一些比 CTypeF 更复杂的东西。您的新 CType 等效项需要将 CTypeF 循环应用到自身。还好，Term为您完成此操作，因此导入 Data.Comp.Term 并将您所有的 CType 替换为 Term CTypeF。 (当然，您可以始终别名 type CType = Term CTypeF 以节省一些输入；请注意 Term CTypeF 与您的原始 CType；您需要在生成和使用 CType 的地方添加一些 Term 构造函数。)

最后，为了在 compdata 中使用统一机制，您需要一个 HasVars 的实例对于将 CVar 构造函数标识为变量的 CTypeF。您还需要使 CTypeF 同时成为 Functor 和 Foldable，但是如果您启用 DeriveFunctor和 DeriveFoldable语言功能，GHC 可以为您做这件事——这是一个严格的机械过程。

---

运行 unify 时，您需要确保在错误 monad m 和变量类型 v 的上下文中执行此操作> 是明确的。有很多方法可以做到这一点，但为了举例，假设我们使用最简单的错误 monad Either e 作为我们的 m，当然你'将希望 v 为 Int。所以你可以这样写:

f = Term (CVar 2)
g = Term CInt

-- By matching against Left and Right, we're letting GHC know that unify
-- should return an Either; this disambiguates `m`
main = case unify [(f, g)] of
  Left _      -> print "did not unify"
  Right subst -> doMoreWork subst

-- The Int here disambiguates `v`
doMoreWork :: Subst CTypeF Int -> IO ()
doMoreWork subst = undefined -- fill in the blank!