Являются ли все контейнеры фиксированного размера сильными моноидальными функторами и / или наоборот?

Класс Applicativeтипов представляет слабые моноидальные функторы, которые сохраняют декартову моноидальную структуру в категории типизированных функций.

Другими словами, учитывая канонические изоморфизмы, свидетельствующие о том, что (,)образуется моноидальная структура:

-- Implementations left to the motivated reader
assoc_fwd :: ((a, b), c) -> (a, (b, c))
assoc_bwd :: (a, (b, c)) -> ((a, b), c)

lunit_fwd :: ((), a) -> a
lunit_bwd :: a -> ((), a)

runit_fwd :: (a, ()) -> a
runit_bwd :: a -> (a, ())

Класс типов и его законы можно эквивалентно записать так:

class Functor f => Applicative f
  where
  zip :: (f a, f b) -> f (a, b)
  husk :: () -> f ()

-- Laws:

-- assoc_fwd >>> bimap id zip >>> zip
-- =
-- bimap zip id >>> zip >>> fmap assoc_fwd

-- lunit_fwd
-- =
-- bimap husk id >>> zip >>> fmap lunit_fwd

-- runit_fwd
-- =
-- bimap id husk >>> zip >>> fmap runit_fwd

Можно было бы удивительно , что функтор , который oplax моноидальный относительно ту же структуру может выглядеть так:

class Functor f => OpApplicative f
  where
  unzip :: f (a, b) -> (f a, f b)
  unhusk :: f () -> ()

-- Laws:

-- assoc_bwd <<< bimap id unzip <<< unzip
-- =
-- bimap unzip id <<< unzip <<< fmap assoc_bwd

-- lunit_bwd
-- =
-- bimap unhusk id <<< unzip <<< fmap lunit_bwd

-- runit_bwd
-- =
-- bimap id unhusk <<< unzip <<< fmap runit_bwd

Если мы думаем о типах, используемых в определениях и законах, неутешительная истина раскрывается; OpApplicativeне более конкретное ограничение, чем Functor:

instance Functor f => OpApplicative f
  where
  unzip fab = (fst <$> fab, snd <$> fab)
  unhusk = const ()

Однако, хотя каждый Applicativeфунктор (на самом деле, любой Functor) тривиален OpApplicative, не обязательно есть хорошие отношения между Applicativeслабостями и OpApplicativeпрозрачностями. Таким образом, мы можем искать сильные моноидальные функторы относительно декартовой моноидальной структуры:

class (Applicative f, OpApplicative f) => StrongApplicative f

-- Laws:
-- unhusk . husk = id
-- husk . unhusk = id
-- zip . unzip = id
-- unzip . zip = id

Первый закон, приведенный выше, тривиален, поскольку единственным обитателем этого типа () -> ()является функция тождественности ().

Тем не менее, оставшиеся три закона, и , следовательно, сам подкласс, является не тривиальной. В частности, не каждый Applicativeявляется законным примером этого класса.

Вот некоторые Applicativeфункторы, для которых мы можем объявить законные случаи StrongApplicative:

• Identity
• VoidF
• (->) r
• Monoid m => (,) m (Посмотри ответы)
• Vec (n :: Nat)
• Stream (Бесконечный)

И вот некоторые Applicativeиз которых мы не можем:

• []
• Either e
• Maybe
• NonEmptyList

Приведенная здесь схема предполагает, что StrongApplicativeкласс в некотором смысле является FixedSizeклассом, где «фиксированный размер» ^* означает, что множественность ^** жителей одного aиз жителей f aявляется фиксированной.

Это можно сформулировать как две гипотезы:

• Каждый Applicativeпредставляющий «фиксированный размер» контейнер элементов своего аргумента типа является экземпляромStrongApplicative
• Не StrongApplicativeсуществует экземпляра, в котором число вхождений aможет варьироваться

Может ли кто-нибудь подумать о контрпримерах, опровергающих эти предположения, или о некоторых убедительных рассуждениях, демонстрирующих, почему они истинны или ложны?

* Я понимаю, что не правильно определил прилагательное «фиксированный размер». К сожалению, задача немного круглая. Я не знаю ни одного формального описания контейнера «фиксированного размера», и пытаюсь придумать его. StrongApplicativeмоя лучшая попытка до сих пор.

Однако, чтобы оценить, является ли это хорошим определением, мне нужно кое-что сравнить с этим. Учитывая некоторое формальное / неформальное определение того, что означает, что функтор имеет заданный размер или кратность по отношению к обитателям аргумента его типа, вопрос заключается в том, StrongApplicativeточно ли существование экземпляра различает функторы фиксированного и переменного размера.

Не зная о существующем формальном определении, я обращаюсь к интуиции при использовании термина «фиксированный размер». Однако, если кто-то уже знает о существующем формализме для размера функтора и может сравниться StrongApplicativeс ним, тем лучше.

** Под «множественностью» я имею в виду в произвольном смысле «сколько» произвольных элементов типа параметра функтора встречается у обитателя типа фомена функтора. Это не имеет отношения к конкретному типу, к которому применяется функтор, и, следовательно, не относится к каким-либо конкретным обитателям типа параметра.

Не точная информация об этом привела к некоторой путанице в комментариях, поэтому вот несколько примеров того, что я бы посчитал размером / множественностью различных функторов:

• VoidF: фиксированный, 0
• Identity: фиксированный, 1
• Maybe: переменная, минимум 0, максимум 1
• []: переменная, минимум 0, максимум бесконечно
• NonEmptyList: переменная, минимум 1, максимум бесконечно
• Stream: фиксированный, бесконечный
• Monoid m => (,) m: фиксированный, 1
• data Pair a = Pair a a: фиксированный, 2
• Either x: переменная, минимум 0, максимум 1
• data Strange a = L a | R a: фиксированный, 1

• Каждый Applicativeпредставляющий «фиксированный размер» контейнер элементов своего аргумента типа является экземпляромStrongApplicative
• Не StrongApplicativeсуществует экземпляра, в котором число вхождений aможет варьироваться

Может ли кто-нибудь подумать о контрпримерах, опровергающих эти предположения, или о некоторых убедительных рассуждениях, демонстрирующих, почему они истинны или ложны?

Я не уверен насчет этой первой гипотезы, и, основываясь на обсуждениях с @AsadSaeeduddin, это, вероятно, будет трудно доказать, но вторая гипотеза верна. Чтобы понять почему, рассмотрим StrongApplicativeзакон husk . unhusk == id; то есть для всех x :: f (), husk (unhusk x) == x. Но в Haskell, unhusk == const ()так что закон равносильно тому, для всех x :: f (), husk () == x. Но это, в свою очередь, подразумевает, что может существовать только одно отдельное значение типа f (): если было два значения x, y :: f (), то x == husk ()и husk () == y, так x == y. Но если существует только одно возможное f ()значение, то оно fдолжно иметь фиксированную форму. (Например, для data Pair a = Pair a a, есть только одно значение типа Pair (), это существо Pair () (), но есть несколько значений типа Maybe ()или [()].) Таким образомhusk . unhusk == idподразумевает, что он fдолжен быть фиксированной формы.

Мы можем ответить хотя бы на один из этих вопросов отрицательно:

Каждый Applicative, представляющий контейнер «фиксированного размера» с элементами своего аргумента типа, является экземпляром StrongApplicative

На самом деле один из примеров законности StrongApplicativeв исходном вопросе неверен. Писатель аппликативен Monoid => (,) mне так StrongApplicative, потому что к примеру husk $ unhusk $ ("foo", ()) == ("", ()) /= ("foo", ()).

Аналогично, пример контейнера фиксированного размера:

data Strange a = L a | R a

фиксированной кратности 1, не является сильным аппликативным, потому что, если мы определяем, husk = Leftто husk $ unhusk $ Right () /= Right (), и наоборот. Эквивалентный способ увидеть это состоит в том, что это всего лишь писатель, применимый для выбора моноида Bool.

Таким образом, существуют аппликативы «фиксированного размера», которых нет StrongApplicative. Все ли StrongApplicatives имеют фиксированный размер, еще неизвестно.

Давайте возьмем представимые функторы в качестве нашего определения «контейнера фиксированного размера»:

class Representable f where
    type Rep f
    tabulate :: (Rep f -> a) -> f a
    index :: f a -> Rep f -> a

Реальное Representableимеет несколько законов и суперклассов, но для целей этого ответа нам действительно нужны только два свойства:

tabulate . index = id
index . tabulate = id

(Хорошо, нам также нужен законопослушный instance StrongApplicative ((->) r). Легко, ты уже согласен, что он существует.)

Если мы примем это определение, то я могу подтвердить эту гипотезу 1:

Каждый Applicativeпредставляющий «фиксированный размер» контейнер элементов своего аргумента типа является [законопослушным] экземпляромStrongApplicative

правда. Вот как:

instance Representable f => Applicative f where
    zip (fa, fb) = tabulate (zip (index fa, index fb))
    husk = tabulate . husk

instance Representable f => OpApplicative f where
    unzip fab = let (fa, fb) = unzip (index fab) in (tabulate fa, tabulate fb)
    unhusk = unhusk . index

instance Representable f => StrongApplicative f

Есть много законов, которые нужно доказать, но я сосредоточусь только на Большой четверке, которая StrongApplicativeдобавляет - вы, вероятно, уже верите в вводные Applicativeи OpApplicative, но если нет, их доказательства выглядят так же, как приведенные ниже ( которые в свою очередь очень похожи друг на друга). Для ясности я буду использовать zipf, huskfи т. Д. Для экземпляра функции, и zipr, huskrи т. Д. Для представимого экземпляра, чтобы вы могли отслеживать, какой есть какой. (И чтобы легко было убедиться, что мы не принимаем то, что пытаемся доказать, как допущение! Это нормально использовать unhuskf . huskf = idпри доказательстве unhuskr . huskr = id, но было бы неправильно предполагать unhuskr . huskr = idэто же доказательство.)

Доказательство каждого закона происходит в основном одинаково: разверните определения, отбросьте изоморфизм, который Representableвам дает, затем используйте аналогичный закон для функций.

unhuskr . huskr
= { def. of unhuskr and huskr }
(unhuskf . index) . (tabulate . huskf)
= { index . tabulate = id }
unhuskf . huskf
= { unhuskf . huskf = id }
id

huskr . unhuskr
= { def. of huskr and unhuskr }
(tabulate . huskf) . (unhuskf . index)
= { huskf . unhuskf = id }
tabulate . index
= { tabulate . index = id }
id

zipr (unzipr fab)
= { def. of unzipr }
zipr (let (fa, fb) = unzipf (index fab) in (tabulate fa, tabulate fb))
= { def. of zipr }
let (fa, fb) = unzipf (index fab) in tabulate (zipf (index (tabulate fa), index (tabulate fb)))
= { index . tabulate = id }
let (fa, fb) = unzipf (index fab) in tabulate (zipf (fa, fb))
= { def. of (fa, fb) }
tabulate (zipf (unzipf (index fab)))
= { zipf . unzipf = id }
tabulate (index fab)
= { tabulate . index = id }
fab

unzipr (zipr (fa, fb))
= { def. of zipr }
unzipr (tabulate (zipf (index fa, index fb)))
= { def. of unzipr }
let (fa', fb') = unzipf (index (tabulate (zipf (index fa, index fb))))
in (tabulate fa', tabulate fb')
= { index . tabulate = id }
let (fa', fb') = unzipf (zipf (index fa, index fb))
in (tabulate fa', tabulate fb')
= { unzipf . zipf = id }
let (fa', fb') = (index fa, index fb)
in (tabulate fa', tabulate fb')
= { def. of fa' and fb' }
(tabulate (index fa), tabulate (index fb))
= { tabulate . index = id }
(fa, fb)