10

类型类Contravariant家族代表了 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

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

  • 不是Contravariant?的类型构造函数
  • 一个类型构造函数，它是 a Contravariant，但不是Divisible?
  • 一个类型构造函数，它是 a Divisible，但不是 a Decidable？
  • 类型构造函数是Decidable?
4

2 回答 2

7

（部分回答）

不是逆变的

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
于 2019-05-14T11:59:17.070 回答
6

（偏导数答案？）

我相信@chi 是正确的，因为他们假设这对所有sConst m都不是合法的，但我是基于对法律的一些猜测。DecidableMonoidmDecidable

在docs中，我们得到了一条Decidable关于法律的诱人提示：

此外，我们期望与通常的协变替代方案 wrt Applicative 满足相同类型的分配律，它应该在某些时候完全制定和添加！

彼此之间应该Decidable并具有什么样的分配关系？Divisible好吧，Divisiblehas chosen，它从接受元素的事物中构建了一个产品接受事物，并且Decidablehas 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)实例memptyforlose和mappendfor choose; 任何其他选择，然后lose不再是一个身份choose。这意味着上述分配律简化为

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

这显然在任意的情况下是虚假Monoid的（尽管，正如 Sjoerd Visscher 所观察到的，在某些Monoids 中是正确的——所以如果是一个分配式幺半群，Const m它仍然可能是合法的）。Decidablem

于 2019-05-14T17:32:37.167 回答