不是逆变/逆变/可分/可判定的好例子？

Question

The Contravariant family of typeclasses 代表 Haskell 生态系统中的标准和基本抽象：

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

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

class Divisible f => Decidable f where
    lose   :: (a -> Void) -> f a
    choose :: (a -> Either b c) -> f b -> f c -> f a

但是，要理解这些类型类背后的概念并不容易。我认为如果您能看到一些反例，将有助于更好地理解这些类型类。因此，本着Good examples of Not a Functor/Functor/Applicative/Monad? 的精神，我正在寻找满足以下要求的数据类型对比示例：

• 不是Contravariant的类型构造函数？
• 类型构造函数是Contravariant，但不是Divisible？
• 类型构造函数是Divisible，但不是Decidable？
• 类型构造函数是Decidable?

Answer 1

（偏导数答案？）

我相信@chi 是正确的when they hypothesize Const m 不可能是所有Monoids m 的合法Decidable，但我基于对Decidable 的一些猜测法律。

在the docs 中，我们在Decidable 法律中得到了这个诱人的提示：

此外，我们期望与通常的协变替代方案（w.r.t Applicative）所满足的分配律相同，应该在某些时候完全制定并添加到这里！

Decidable 和Divisible 之间应该有什么样的分配关系？嗯，Divisible 有 chosen，它从接受元素的东西中构建了一个产品接受的东西，Decidable 有 divided，它从接受元素的东西中构建了一个接受总和的东西。由于产品分布在总和之上，也许我们正在寻求的规律将f (a, Either b c) 与f (Either (a, b) (a, c)) 相关联，它们的值可以分别通过a `divided` (b `chosen` c) 和(a `divided` b) `chosen` (a `divided` c) 构造。

所以我假设缺少的Decidable 法律类似于

a `divided` (b `chosen` c) = contramap f ((a `divided` b) `chosen` (a `divided` c))
  where f (x, y) = bimap ((,) x) ((,) x) y

这对于Predicate、Equivalence 和Op 确实很满意（到目前为止，我花时间检查了三个Decidable 实例）。

现在我相信你可以拥有的唯一实例 instance Monoid m => Decidable (Const m) 使用 mempty 代表 lose 和 mappend 代表 choose;任何其他选择，然后lose 不再是choose 的标识。这意味着上述分配律简化为

a `mappend` (b `mappend` c) = (a `mappend` b) `mappend` (a `mappend` c)

这显然是伪造的在任意Monoid 中不正确（尽管，正如Sjoerd Visscher 所观察到的，在某些Monoids 中是正确的——所以Const m 仍然可以是合法的@987654356 @ 如果m 是一个分布幺半群）。

Answer 2

（部分回答）

非逆变

newtype F a = K (Bool -> a)

不是逆变的（但是，它是一个协变函子）。

逆变，但不可整除

newtype F a = F { runF :: a -> Void }

是逆变的，但它不能是Divisible，否则

runF (conquer :: F ()) () :: Void

关于“可分但不可判定”的说明

对于不可判定的整除数，我没有合理的例子。我们可以观察到这样的反例一定是这样的，因为它违反了法律，而不仅仅是类型签名。确实，如果Divisible F 成立，

instance Decidable F where
    lose _ = conquer
    choose _ _ _ = conquer

满足方法的类型签名。

在库中，我们发现 Const m 是一个整除数，而 m 是一个幺半群。

instance Monoid m => Divisible (Const m) where
  divide _ (Const a) (Const b) = Const (mappend a b)
  conquer = Const mempty

也许这不能是合法的Decidable？ （我不确定，它似乎满足 Decidable 法律，但库中没有 Decidable (Const m) 实例。）

可判定

取自图书馆：

newtype Predicate a = Predicate (a -> Bool)

instance Divisible Predicate where
  divide f (Predicate g) (Predicate h) = Predicate $ \a -> case f a of
    (b, c) -> g b && h c
  conquer = Predicate $ const True

instance Decidable Predicate where
  lose f = Predicate $ \a -> absurd (f a)
  choose f (Predicate g) (Predicate h) = Predicate $ either g h . f