从连词中提取约束

Question

这是一个布尔谓词树。

data Pred a = Leaf (a -> Bool)
            | And (Pred a) (Pred a)
            | Or (Pred a) (Pred a)
            | Not (Pred a)

eval :: Pred a -> a -> Bool
eval (Leaf f) = f
eval (l `And` r) = \x -> eval l x && eval r x
eval (l `Or` r) = \x -> eval l x || eval r x
eval (Not p) = not . eval p

这个实现很简单，但问题是不同类型的谓词不能组合。博客系统的玩具示例：

data User = U {
    isActive :: Bool
}
data Post = P {
    isPublic :: Bool
}

userIsActive :: Pred User
userIsActive = Leaf isActive

postIsPublic :: Pred Post
postIsPublic = Leaf isPublic

-- doesn't compile because And requires predicates on the same type
-- userCanComment = userIsActive `And` postIsPublic

您可以通过定义data World = W User Post 之类的内容并专门使用Pred World 来解决此问题。但是，向您的系统添加新实体则需要更改 World；而较小的谓词通常不需要全部内容（postIsPublic 不需要使用User）；在没有Post 的上下文中的客户端代码不能使用Pred World。

---

它在 Scala 中很有魅力，它会很高兴地通过统一推断组合特征的子类型约束：

sealed trait Pred[-A]
case class Leaf[A](f : A => Boolean) extends Pred[A]
case class And[A](l : Pred[A], r : Pred[A]) extends Pred[A]
case class Or[A](l : Pred[A], r : Pred[A]) extends Pred[A]
case class Not[A](p : Pred[A]) extends Pred[A]

def eval[A](p : Pred[A], x : A) : Boolean = {
  p match {
    case Leaf(f) => f(x)
    case And(l, r) => eval(l, x) && eval(r, x)
    case Or(l, r) => eval(l, x) || eval(r, x)
    case Not(pred) => ! eval(pred, x)
  }
}

class User(val isActive : Boolean)
class Post(val isPublic : Boolean)

trait HasUser {
  val user : User
}
trait HasPost {
  val post : Post
}

val userIsActive = Leaf[HasUser](x => x.user.isActive)
val postIsPublic = Leaf[HasPost](x => x.post.isPublic)
val userCanCommentOnPost = And(userIsActive, postIsPublic)  // type is inferred as And[HasUser with HasPost]

（这是因为 Pred 被声明为逆变的 - 无论如何都是这样。）当你需要 eval 和 Pred 时，你可以简单地将所需的特征组合成一个匿名子类 - new HasUser with HasPost { val user = new User(true); val post = new Post(false); }

---

我想我可以通过将特征转换为类并将 Pred 参数化为它需要的类型类而不是它所操作的具体类型来将其转换为 Haskell。

-- conjunction of partially-applied constraints
-- (/\) :: (k -> Constraint) -> (k -> Constraint) -> (k -> Constraint)
type family (/\) c1 c2 a :: Constraint where
    (/\) c1 c2 a = (c1 a, c2 a)

data Pred c where
    Leaf :: (forall a. c a => a -> Bool) -> Pred c
    And :: Pred c1 -> Pred c2 -> Pred (c1 /\ c2)
    Or :: Pred c1 -> Pred c2 -> Pred (c1 /\ c2)
    Not :: Pred c -> Pred c

data User = U {
    isActive :: Bool
}
data Post = P {
    isPublic :: Bool
}

class HasUser a where
    user :: a -> User
class HasPost a where
    post :: a -> Post

userIsActive :: Pred HasUser
userIsActive = Leaf (isActive . user)

postIsPublic :: Pred HasPost
postIsPublic = Leaf (isPublic . post)

userCanComment = userIsActive `And` postIsPublic
-- ghci> :t userCanComment
-- userCanComment :: Pred (HasUser /\ HasPost)

这个想法是每次使用Leaf 时，您都对整体的类型定义了一个要求（例如HasUser），而无需直接指定该类型。树的其他构造函数将这些要求向上冒泡（使用约束结合/\），因此树的根知道叶子的所有要求。然后，当你想eval你的谓词时，你可以组成一个包含谓词需要的所有数据的类型（或使用元组），并使其成为所需类的实例。

但是，我不知道怎么写eval：

eval :: c a => Pred c -> a -> Bool
eval (Leaf f) = f
eval (l `And` r) = \x -> eval l x && eval r x
eval (l `Or` r) = \x -> eval l x || eval r x
eval (Not p) = not . eval p

出错的是And 和Or 案例。 GHC 似乎不愿意在递归调用中扩展/\：

Could not deduce (c1 a) arising from a use of ‘eval’
from the context (c a)
  bound by the type signature for
             eval :: (c a) => Pred c -> a -> Bool
  at spec.hs:55:9-34
or from (c ~ (c1 /\ c2))
  bound by a pattern with constructor
             And :: forall (c1 :: * -> Constraint) (c2 :: * -> Constraint).
                    Pred c1 -> Pred c2 -> Pred (c1 /\ c2),
           in an equation for ‘eval’
  at spec.hs:57:7-15
Relevant bindings include
  x :: a (bound at spec.hs:57:21)
  l :: Pred c1 (bound at spec.hs:57:7)
  eval :: Pred c -> a -> Bool (bound at spec.hs:56:1)
In the first argument of ‘(&&)’, namely ‘eval l x’
In the expression: eval l x && eval r x
In the expression: \ x -> eval l x && eval r x

GHC 知道c a 和c ~ (c1 /\ c2)（因此知道(c1 /\ c2) a）但不能推导出c1 a，这需要扩展/\ 的定义。我有一种感觉，如果 /\ 是类型 synonym，而不是 family，那么它会起作用，但是 Haskell 不允许部分应用类型同义词（这是在Pred的定义）。

---

我尝试使用constraints 对其进行修补：

conjL :: (c1 /\ c2) a :- c1 a
conjL = Sub Dict
conjR :: (c1 /\ c2) a :- c1 a
conjR = Sub Dict

eval :: c a => Pred c -> a -> Bool
eval (Leaf f) = f
eval (l `And` r) = \x -> (eval l x \\ conjL) && (eval r x \\ conjR)
eval (l `Or` r) = \x -> (eval l x \\ conjL) || (eval r x \\ conjR)
eval (Not p) = not . eval p

不仅...

Could not deduce (c3 a) arising from a use of ‘eval’
from the context (c a)
  bound by the type signature for
             eval :: (c a) => Pred c -> a -> Bool
  at spec.hs:57:9-34
or from (c ~ (c3 /\ c4))
  bound by a pattern with constructor
             And :: forall (c1 :: * -> Constraint) (c2 :: * -> Constraint).
                    Pred c1 -> Pred c2 -> Pred (c1 /\ c2),
           in an equation for ‘eval’
  at spec.hs:59:7-15
or from (c10 a0)
  bound by a type expected by the context: (c10 a0) => Bool
  at spec.hs:59:27-43
Relevant bindings include
  x :: a (bound at spec.hs:59:21)
  l :: Pred c3 (bound at spec.hs:59:7)
  eval :: Pred c -> a -> Bool (bound at spec.hs:58:1)
In the first argument of ‘(\\)’, namely ‘eval l x’
In the first argument of ‘(&&)’, namely ‘(eval l x \\ conjL)’
In the expression: (eval l x \\ conjL) && (eval r x \\ conjR)

还有……

Could not deduce (c10 a0, c20 a0) arising from a use of ‘\\’
from the context (c a)
  bound by the type signature for
             eval :: (c a) => Pred c -> a -> Bool
  at spec.hs:57:9-34
or from (c ~ (c3 /\ c4))
  bound by a pattern with constructor
             And :: forall (c1 :: * -> Constraint) (c2 :: * -> Constraint).
                    Pred c1 -> Pred c2 -> Pred (c1 /\ c2),
           in an equation for ‘eval’
  at spec.hs:59:7-15
In the first argument of ‘(&&)’, namely ‘(eval l x \\ conjL)’
In the expression: (eval l x \\ conjL) && (eval r x \\ conjR)
In the expression:
  \ x -> (eval l x \\ conjL) && (eval r x \\ conjR)

情况大致相同，只是现在 GHC 似乎也不愿意将 GADT 引入的变量与conjL 要求的变量统一起来。 这次conjL类型中的/\已扩展为(c10 a0, c20 a0)。 （我认为这是因为/\ 在conjL 中完全应用，而不是在And 中的咖喱形式。）

不用说，Scala 在这方面比 Haskell 做得更好让我感到惊讶。在检查类型之前，我该如何摆弄eval 的正文？我可以哄 GHC 扩展/\ 吗？我是不是走错了路？我想要的可能吗？

Answer 1

数据构造函数And :: Pred c1 -> Pred c2 -> Pred (c1 /\ c2) 和Or :: ... 格式不正确，因为无法部分应用类型族。但是，早于 7.10 的 GHC 将 erroneously accept this definition - 然后在您尝试对其执行任何操作时给出您看到的错误。

你应该使用类而不是类型族；例如

class (c1 a, c2 a) => (/\) (c1 :: k -> Constraint) (c2 :: k -> Constraint) (a :: k)
instance (c1 a, c2 a) => (c1 /\ c2) a 

eval 的直接实现将起作用。