从连接中提取约束

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被声明为逆变 - 它无论如何.)当你需要evala时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扩张/\吗？我是以错误的方式去做的吗？我想要的甚至可能吗？

Answer 1

数据构造函数And :: Pred c1 -> Pred c2 -> Pred (c1 /\ c2)并Or :: ...没有很好地形成,因为不能部分应用类型族.但是,早于7.10的GHC将错误地接受这个定义 - 然后在你尝试对它做任何事情时给出你看到的错误.

你应该使用一个类而不是一个类型系列; 例如

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

并且直接实施eval将工作.