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

Question

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

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

-- 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 (бесконечно)

А вот некоторые Applicatives, для которых мы не можем:

• []
• Either e
• Maybe
• NonEmptyList

Здесь шаблон предполагает, что StrongApplicative класс в некотором смысле FixedSizeкласс, где "фиксированный размер" ^* означает, что множественность ^** жителейa у жителя f a фиксированный.

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

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

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

---

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

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

Не зная о существующем формальном определении, я обращаюсь к интуиции в использовании термина "фиксированный размер". Однако, если кто-то уже знает о существующем формализме размера функтора и может сравнить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

Answer 1

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

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

Я не уверен в этой первой гипотезе и, основываясь на обсуждениях с @AsadSaeeduddin, вероятно, будет трудно доказать, но вторая гипотеза верна. Чтобы понять почему, рассмотримStrongApplicative закон husk . unhusk == id; то есть для всехx :: f (), husk (unhusk x) == x. Но в Haskellunhusk == 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 должен иметь фиксированную форму.

Answer 2

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

Каждый 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 фиксированного размера, еще предстоит выяснить.

Answer 3

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

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). Easy peasy, вы уже согласны с тем, что он существует.)

Если мы примем это определение, то я могу подтвердить эту гипотезу 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)