使用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

因为我是哈斯克尔的新手，所以我不能马上弄清楚我是否可以直接应用它。我可以使用这个库吗?还是建议我从头开始编写整体字？

更新

我目前正在对代码进行以下修改，但是对该方程的统一错误

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-equivalent需要循环地将CTypeF应用于自身。幸运的是，Term为您做到了这一点，因此导入Data.Comp.Term并将所有的CType替换为Term CTypeF。(当然，您可以使用别名type CType = Term CTypeF来保存一些类型；只需注意Term CTypeF与原始CType不完全相同；您需要向生成和使用CType的地方添加一些Term构造函数。)

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

在运行unify时，需要确保在error monad m和变量类型v是明确的上下文中执行该操作。有很多方法可以做到这一点，但为了示例起见，假设我们使用最简单的错误单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!