scala - 从连词中提取约束

这是一棵 bool 谓词树。

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 ，这需要扩展 /\ 的定义。我有一种感觉，如果 /\ 是一个类型同义词，而不是一个家庭，它会起作用，但是 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 扩展 /\ 吗？我是不是用错了方法？我想要的甚至可能吗？

最佳答案

数据构造函数 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 的直接实现将起作用。

关于scala - 从连词中提取约束，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/30821013/