Является ли закон распределения функторов для класса типов `Alt 'тривиальным? - PullRequest
Новая
       10

Является ли закон распределения функторов для класса типов `Alt 'тривиальным?

7 голосов
/ 24 февраля 2020

Я искал l aws для Alt класса типов , который выглядит следующим образом: 

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

Один из l aws выглядит следующим образом: 

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

Ответы [ 2 ]

4 голосов
/ 25 февраля 2020

Хотя это не единодушное отношение к другим ответам и комментариям, это не естественное свойство "реального мира" Haskell.

Это полезно для разработчиков которые пишут непараметрический код c, чтобы знать, когда они должны добавить ограничения, чтобы оставаться совместимыми с кодом, который принимает параметричность как должное.

Пример с плохим поведением 

{-# 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
  (<!>) = (<++>)
3 голосов
/ 25 февраля 2020

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

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

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

  2. Вы захотите иметь эти l aws, если будете переносить эти интерфейсы на языки с системами более слабого типа.

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

...