Haskell为类和实例提供了正确的类型

Question

我正在努力描述重写术语和文字（一阶逻辑）意味着什么。即我想要一个可以在术语和文字上调用的函数applySubstitution。我认为替换可以表示为一个函数。但是，我使用以下代码获得严格的类型变量错误。

{-# LANGUAGE UnicodeSyntax #-}

module Miniexample where
import qualified Data.Maybe as M

data Term a = F a [Term a]
            | V a

data Literal a = P a [Term a]
               | E (Term a) (Term a)

class Substitutable b where
  substitute :: b -> (Term a -> Maybe (Term a)) -> b

instance Substitutable (Term a) where
  substitute x@(V _) σ    = M.fromMaybe x (σ x)
  substitute f@(F l xs) σ = M.fromMaybe f' (σ f)
    where f' = F l (map (flip substitute σ) xs)

instance Substitutable (Literal a) where
  substitute (P l xs) σ = P l (map (flip substitute σ) xs)
  substitute (E s t) σ  = E (substitute s σ) (substitute t σ)

class Substitution σ where
  asSub :: σ -> (a -> Maybe a)

applySubstitution σ t = substitute t (asSub σ)

(<|) t σ = applySubstitution σ t

这给出了以下错误：

• Couldn't match type ‘a1’ with ‘a’
  ‘a1’ is a rigid type variable bound by
    the type signature for:
      substitute :: forall a1.
                    Term a -> (Term a1 -> Maybe (Term a1)) -> Term a
    at /.../Miniexample.hs:16:3-12
  ‘a’ is a rigid type variable bound by
    the instance declaration
    at /.../Miniexample.hs:15:10-31
  Expected type: Term a1
    Actual type: Term a
• In the first argument of ‘σ’, namely ‘x’
  In the second argument of ‘M.fromMaybe’, namely ‘(σ x)’
  In the expression: M.fromMaybe x (σ x)
• Relevant bindings include
    σ :: Term a1 -> Maybe (Term a1)
      (bound at /.../Miniexample.hs:16:22)
    x :: Term a
      (bound at /.../Miniexample.hs:16:14)
    substitute :: Term a -> (Term a1 -> Maybe (Term a1)) -> Term a
      (bound at /.../Miniexample.hs:16:3)

在我的脑海中，b类中的类型变量Substitutable应该能够承担Term a的值（我确定的坏术语）。

任何提示都将非常受欢迎。

为了给出一个更具体的例子，下面的工作，但需要明确哪个函数applyTermSub或applyLitSub调用，其次，替换映射的实现泄漏到更一般的过程的实现。

module Miniexample where
import qualified Data.Maybe as M
import qualified Data.List as L

data Term a = F a [Term a]
            | V a deriving (Eq)

data Literal a = P a [Term a]
               | E (Term a) (Term a) deriving (Eq)


termSubstitute :: (Term a -> Maybe (Term a)) -> Term a -> Term a
termSubstitute σ x@(V _)    = M.fromMaybe x (σ x)
termSubstitute σ f@(F l xs) = M.fromMaybe f' (σ f)
    where f' = F l (map (termSubstitute σ) xs)

litSubstitute :: (Term a -> Maybe (Term a)) -> Literal a -> Literal a
litSubstitute σ (P l xs) = P l (map (termSubstitute σ) xs)
litSubstitute σ (E s t)  = E (termSubstitute σ s) (termSubstitute σ t)

applyTermSub :: (Eq a) => Term a -> [(Term a, Term a)] -> Term a
applyTermSub t σ = termSubstitute (flip L.lookup σ) t

applyLitSub :: (Eq a) => Literal a -> [(Term a, Term a)] -> Literal a
applyLitSub l σ = litSubstitute (flip L.lookup σ) l

-- variables
x  = V "x"
y  = V "y"
-- constants
a  = F "a" []
b  = F "b" []
-- functions
fa = F "f" [a]
fx = F "f" [x]

σ = [(x,y), (fx, fa)]

test = (applyLitSub (P "p" [x, b, fx]) σ) == (P "p" [y, b, fa])

理想情况下，我希望有一个替换接口（即一个可以使用Data.Map等），其次我想要一个替代函数来捕获术语和文字。

Answer 1

你得到的错误是Term a指定的instance Substitutable (Term a)与Term a接受的σ不同的抱怨。这是因为Haskell量化了a函数的substitute，但没有超过实例定义的其余部分。所以substitute的实现必须接受σ处理Term a1的a1的某些值，这不保证是你的实例定义的特定a。 （是的，您的实例是在所有a上定义的......但是从实例定义的范围内，就好像选择了特定的a一样。）

您可以通过类型构造函数而不仅仅是类型来参数化Substitutable类，并将相同的a传递给σ类型中使用的类型构造函数来避免这种情况。

{-# LANGUAGE UnicodeSyntax #-}

import qualified Data.Maybe as M
import qualified Data.List as L

data Term a = F a [Term a]
            | V a deriving (Eq)

data Literal a = P a [Term a]
               | E (Term a) (Term a) deriving (Eq)

class Substitutable f where
  substitute :: f a -> (Term a -> Maybe (Term a)) -> f a

instance Substitutable Term where
  substitute x@(V _) σ    = M.fromMaybe x (σ x)
  substitute f@(F l xs) σ = M.fromMaybe f' (σ f)
    where f' = F l (map (flip substitute σ) xs)

instance Substitutable Literal where
  substitute (P l xs) σ = P l (map (flip substitute σ) xs)
  substitute (E s t) σ  = E (substitute s σ) (substitute t σ)

(<|) t σ = substitute t $ flip L.lookup σ


-- variables
x  = V "x"
y  = V "y"
-- constants
a  = F "a" []
b  = F "b" []
-- functions
fa = F "f" [a]
fx = F "f" [x]

σ = [(x,y), (fx, fa)]


main = print $ show $ (P "p" [x, b, fx] <| σ) == P "p" [y, b, fa]