将谓词类型实现为逆变单子？

Question

我很确定我可以证明，原则上，Predicate 类型构造函数是 ContraMonad，是 Monad 的泛化，其中函子是逆变的，但我不确定它会如何实施。

首先，让我们定义一些术语：

class Contravariant f where
    contramap :: (b -> a) -> f a -> f b

class ContraMonad m where
    return :: a -> m a
    join :: m(m a) -> m a
    contrabind :: m a -> (m b -> a) -> m b

data Predicate a = Pred {getPred :: a -> Bool}

instance Contravariant Predicate where
    contramap f x = Pred ((getPred x).f)

这表明谓词是一个从 a 取值并从中生成命题的函数，是从 Hask 到 Hask^{op} 的逆变函子。谓词的一个例子是：

isEven :: Integer -> Bool
isEven n = if (mod n 2 == 0)
           then True
           else False

函数isEven 是数学意义上的谓词，而Pred isEven 是此处实现的意义上的Predicate。

将Predicate 实现为ContraMonad 比较棘手。

return只有一种自然选择。

return :: a -> Predicate a
return x = Pred(const True)

您可能会考虑“返回”给出一个谓词的可能性，该谓词 x 为真，并且没有其他类型为 a 的元素为真。问题是只有当 a 是 Eq 类型类的成员时才能实现。

考虑加入比contrabind 更容易。显然，我们想要

contrabind x f = join.contramap f x

这样 contrabind 在考虑 f 作为逆变函子的同时尽可能地类似于 bind。函数f 将Pred b 转换为a，因此contramap f 将Pred a 转换为Pred(Pred b)。

那么，join 应该怎么做呢？它必须将 a 类型的谓词的谓词转换为 a 类型的谓词。 a 类型谓词的谓词对 a 类型的谓词进行判断。例如，考虑 a = Integer。 Pred( Pred Integer) 的一个例子是：

Pred("The predicate f is true for all even numbers.")

我用引号代替了实际的实现。如果 f 对所有偶数都为真，则此陈述为真。例如，Pred isEven 的计算结果为 True。

考虑到集合 A 上的谓词对应于 A 的子集这一事实，Pred(Pred A) 是一个函数的包装器，它采用 A 的所有子集并将它们判断为“真”或“假”。我们希望join 给我们一个谓词，这与给A 的一个子集相同。这个子集应该尽可能无损。事实上，它应该关心每一个Pred X 的真值，w.r.t. Pred(Pred X) 判断。在我看来，自然的解决方案似乎是所有被判断为“真”的子集的交集，这与将所有真谓词“与”在一起

predAnd :: (a -> Bool) -> (a -> Bool) -> (a -> Bool)
predAnd p q = \x -> ((getPred p) $ x) && ((getPred q) $ x)

作为一个例子，让我们回到“谓词 f 对所有偶数都为真”。在此判断下，每个被评估为True 的谓词对于所有偶数都必须为真，因此每个可能的子集都包含偶数。所有这些集合的交集将只是偶数集合，因此join 将返回谓词Pred isEven。

我的问题是，“加入”实际上是如何实现的？可以实施吗？我可以看到对于像“整数”这样的无限类型产生的不可判定集的潜在问题，但它甚至可以为像“Char”这样的有限类型实现，即使幂集也具有有限的基数？

Answer 1

有一点相关，Applicative的逆变版本是Divisible，我这里简化了

class Contravariant f => Divisible f where
  divide  :: f b -> f c -> f (b, c)
  conquer :: f a

Data.Functor.Contravariant.Divisible 中的divide 是用a -> (b, c) 编写的，这突出了将a 的工作划分为b 和c 的工作的想法。

{-# LANGUAGE RankNTypes #-}

-- The divide from Data.Functor.Contravariant.Divisible
divide' :: Divisible f => (a -> (b, c)) -> f b -> f c -> f a
divide' f b c = contramap f $ divide b c

-- And a proof they types are equivalent
proof :: (forall a b c. (a -> (b, c)) -> f b -> f c -> f a) -> f b -> f c -> f (b, c)
proof divide' = divide' id

如果结果是Monoid，则任何Op 都是Divisible。这是Predicate的泛化，也就是OpAll

import Data.Monoid

newtype Op r a = Op {runOp :: a -> r}

instance Contravariant (Op r) where
  contramap f (Op g) = Op (g . f)

instance Monoid r => Divisible (Op r) where
  divide (Op f) (Op g) = Op (\(b, c) -> f b <> g c)
  conquer = Op (const mempty)

---

作为奖励，Op r 是 Monoid，只要结果 r 是一个 moniod，它提供了一种直接定义 predAnd 的方法

instance Monoid a => Monoid (Op a b) where
  mempty = Op (const mempty)
  mappend (Op p) (Op q) = Op $ \a -> mappend (p a) (q a)

type Predicate a = Op All a

predAnd :: Predicate a -> Predicate a -> Predicate a
predAnd = mappend 

但那是hardly surprising。

Answer 2

我想我可能已经想到了我自己问题的部分答案。首先，我们必须强制 a 在 Eq 类型类中。

join p = Pred(\x -> not ((getPred p) (\y -> y /= x)))

这是一个谓词，它接受a 类型的元素并从中构造一个谓词，即x 为假而其他一切都为真的谓词。然后根据原来的Pred( Pred a)判断对这个谓词求值。

如果此谓词为真，则表示 x 不在所有谓词的交集中，因此最终谓词将 x 发送为 False。另一方面，如果这个谓词是假的，那么x就不一定在交集里，除非我们做一个额外的规则：

如果Pred( Pred a)判断判定近最大谓词为假，则该近最大谓词判定为假的元素必须出现在所有判断为真的谓词中。

因此，判断“谓词 f 对所有偶数都为真”。在此规则下是允许的，但判断“谓词 f 仅对偶数为真”。不被允许。如果使用第一类判断，join 将给出所有真谓词的交集。在第二种情况下，join 将简单地给出一个谓词，它有时可以告诉您x 是否不必要。如果它返回False，x 肯定是没有必要的。如果返回True，则测试没有结果。

我现在确信，除非 a 类型是有限的，否则“ANDing”的完整实现是不可能的，即使这样也是不切实际的，除非 a 非常小。