Тривиален ли закон распределения функторов для класса типов ʻAlt`?

Question

Я смотрел на законы о Alttypeclass, который выглядит так:

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 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 что это проверка типов, но будет ли отклонено законом?

Answer 1

Да, закон действует бесплатно, по параметричности.

Даже тогда эти законы все еще имеют значение.

1. Это позволяет людям знать о них, не будучи адептами теории языков программирования.

2. Вы захотите, чтобы эти законы были рядом, если вы переносите эти интерфейсы на языки с более слабыми системами типов.

3. Пока Haskell не получит формальную семантику, мы технически не знаем, что эти бесплатные теоремы верны. По достаточно высоким стандартам формальности недостаточно делать вид, что Haskell является чистым полиморфным лямбда-исчислением. Так что мы могли бы на всякий случай добавить и проверить эти "бесплатные" законы.

Answer 2

Хотя это не является консенсусом других ответов и комментариев, это не является естественным свойством "реального" 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
  (<!>) = (<++>)