從連接中提取約束

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中的一個魅力所在，它會很樂意通過統一推斷組成性狀亞型限制：（這工作，因爲Pred被聲明爲逆變 - 這是無論如何）

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] 

當你需要一個evalPred，你可以簡單地構成所需的特性轉化爲一個匿名子類 - new HasUser with HasPost { val user = new User(true); val post = new Post(false); }

---

我想我可以把它轉換成Haskell，把它轉化爲類，並通過它需要的類型參數化Pred，而不是它操作的具體類型。

-- 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 :: 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 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 a也似乎不願意將GADT帶來的變量與conjL所要求的變量統一起來。它看起來像這個時間/\中的conjL類型已將擴大到(c10 a0, c20 a0)。 （我想這是因爲/\出現在conjL完全適用，不是咖喱形式，它And一樣。）

不用說，這是令人驚訝的，我認爲斯卡拉做到這一點比哈斯克爾更好。我怎麼能擺弄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將工作。