从连词中提取约束

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 你的谓词时，你可以组成一个包含谓词需要的所有数据的类型（或使用元组）并使其成为所需类.[=57= 的实例]

可是我想不通怎么写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 不会t 允许部分应用类型同义词（这在 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 做得更好。我如何 fiddle 使用 eval 的主体直到它进行类型检查？我可以哄 GHC 扩展 /\ 吗？我会以错误的方式去做吗？我想要的有可能吗？

Answer 1

数据构造函数 And :: Pred c1 -> Pred c2 -> Pred (c1 /\ c2) 和 Or :: ... 格式不正确，因为类型族不能部分应用。然而，早于 7.10 的 GHC 将 erroneously accept this definition - 然后给出当你尝试用它做任何事情时看到的错误。

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

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

eval 的直接实施将起作用。

从连词中提取约束

Extracting a constraint from a conjunction

haskell

types

scala

type-constraints