`Alt` 类型类的函子分布规律是否微不足道？

Question

我正在查看 the Alt typeclass 的法律，它看起来像这样：

class Functor f => Alt f
  where
  (<!>) :: f a -> f a -> f a

其中一条定律是这样的：

<$> left-distributes over <!>:  f <$> (a <!> b) = (f <$> a) <!> (f <$> b)

更详细地说，这是：

fmap f $ (<!>) a b = (<!>) (fmap f a) (fmap f b)

假设我们取消 <!> 操作，即我们假设 class 是这样写的：

class Functor f => Alt f
  where
  alt :: (f a, f a) -> f a

我们可以这样写一个组合器：

mapBoth :: Functor f => (a -> b) -> (f a, f a) -> (f b, f b)
mapBoth f = bimap (fmap f) (fmap f)

这表示 type Pair a = (a, a) 函子与给定函子 f 的组合。所以它本身就是一个函子的态射映射。

有问题的法律现在可以这样写（不改变其含义）：

fmap f . alt = alt . mapBoth f

请注意，mapBoth f 只是将 fmap f 应用于 alt 的两个论点，就像法律的原始陈述一样。

这类似于要求 alt 是从函子 (f -, f -) 到函子 f - 的自然转换。

但是，alt的类型的函数不是类型的函数实际上不是不可能是自然变换吗？如何编写一个 alt 的 "bad" 实现来进行类型检查，但会被法律拒绝？

Answer 1

是的，通过参数化，定律是免费的。

即便如此，这些法律仍然有价值。

即使不是编程语言理论的人也能知道它们。
如果您将这些接口移植到类型系统较弱的语言，您将希望遵守这些法律。
直到 Haskell 实际上被赋予形式语义，我们在技术上不知道那些自由定理是否成立。通过足够高的形式标准，假装 Haskell 是纯多态 lambda 演算是不够的。所以我们不妨添加和检查这些"free"法律以防万一

Answer 2

虽然这不是其他答案和评论的共识，但这不是 "real-world" Haskell 的自然属性 .

对于编写非参数代码的开发人员来说，了解他们何时应该添加约束以保持与将参数性视为理所当然的代码兼容是很有帮助的。

行为不端的例子

{-# LANGUAGE GADTs #-}

data Badly a where
  End :: a -> Badly a
  Cons :: a -> Badly b -> Badly a

(<++>) :: Badly a -> Badly b -> Badly a
(End a)    <++> r = Cons a r
(Cons a l) <++> r = Cons a (l <++> r)

instance Functor Badly where
  fmap f (End a) = End (f a)
  fmap f (Cons a r) = Cons (f a) r

instance Alt f where
  (<!>) = (<++>)

`Alt` 类型类的函子分布规律是否微不足道？

Is the functor distribution law for the `Alt` typeclass trivial?

haskell

functor

free-theorem

行为不端的例子