Понимание диаграмм Продукта и Копродукции

Question

Я пытаюсь понять Product и Coproduct, соответствующие следующей картинке:

Продукт:

Копродукция:

Как я понимаю, тип Product в Haskell, например:

data Pair = P Int Double

и тип Sum:

data Pair = I Int | D Double 

Как понять изображения, относящиеся к типам Sum и Product?

Изображения из http://blog.higher -order.com / blog / 2014/03/19/monoid-morphisms-products-coproducts/.

Answer 1

Продукт (Tuple в Хаскеле) - это объект с двумя проекциями . Это функции проецирования продукта на их индивидуальные факторы fst и snd.

С другой стороны, копродукция (Either в Хаскеле) - это объект, имеющий две инъекции . Это функции , вводящие отдельные слагаемые lefts и rights в сумму.

Обратите внимание, что и продукт, и сопутствующий продукт должны соответствовать универсальному свойству. Я рекомендую Бароша Милевского введение по этой теме вместе с его лекцией .

Answer 2

Итак, насколько я могу судить, идея этих диаграмм заключается в том, что вам даны:

• типы A, B и Z
• функцияf и g указанных типов (на первой диаграмме f :: Z -> A и g :: Z -> B, на второй стрелки идут «в другую сторону», поэтому f :: A -> Z и g :: B -> Z).

Сейчас я сконцентрируюсь на первой диаграмме, чтобы мне не приходилось говорить все дважды с небольшими вариациями.

В любом случае, учитывая вышеизложенное, идея заключается в том, что существуеттип M вместе с функциями fst :: M -> A, snd :: M -> B и h :: Z -> M, так что, как говорят математики, диаграмма "коммутирует".Под этим просто подразумевается, что с учетом любых двух точек на диаграмме, если вы будете следовать стрелкам каким-либо образом от одной к другой, результирующие функции будут одинаковыми.То есть f - это то же самое, что и fst . h, а g - это то же самое, что и snd . h

Легко видеть, что независимо от того, что Z, тип пары (A, B) вместе с обычными функциями Haskell fst и snd удовлетворяет это - вместе с соответствующим выбором h, а именно:

h z = (f z, g z)

, который тривиально удовлетворяет двум требуемым тождествам длядиаграмма для коммутирования.

Это базовое объяснение диаграммы.Но вы можете быть немного озадачены ролью Z во всем этом.Это возникает потому, что то, что на самом деле говорится, довольно сильно.Это то, что, учитывая A, B, f и g, существует M вместе с функциями fst и snd, что вы можете построить такую ​​диаграмму для любого type Z (что также означает предоставление функции h :: Z -> M).И далее, что есть только одна функция h, которая удовлетворяет требуемым свойствам.

Довольно ясно, как только вы поиграете с ней и поймете различные требования, эта пара (A, B)и различные другие типы, изоморфные ему (что в основном означает MyPair A B, где вы определили data MyPair a b = MyPair a b), являются единственными вещами, которые удовлетворяют этому.И что есть другие типы M, которые также будут работать, но которые дадут различные различные h s - например.принять M как тройное (A, B, Int), с fst и snd извлечением ("проецированием" в математической терминологии) первого и второго компонентов, а затем h z = (f z, g z, x) является такой функцией для любого x :: Intчто вы хотите назвать.

Прошло слишком много времени с тех пор, как я изучал математику и, в частности, теорию категорий, чтобы доказать, что пара (A, B) является единственным типом, который удовлетворяет "универсальному свойству", которое мыВы говорите - но будьте уверены, что это так, и вам действительно не нужно это понимать (или вообще что-либо из этого), чтобы иметь возможность программировать с типами товаров и сумм в Haskell.

Вторая диаграмма более или менее такая же, но со всеми перевернутыми стрелками.В этом случае «копроцесс» или «сумма» M из A и B оказывается Either a b (или чем-то изоморфным для него), и h :: M -> Z будет определяться как:

h (Left a) = f a
h (Right b) = g b

Answer 3

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

Итак, продукт говорит:

1. Вы даете мнедва объекта, A и B.
2. Я даю вам новый объект M, и две стрелки fst: M -> A и snd: M -> B.
3. Вы даете мне объект Zи две стрелки f: Z -> A и g: Z -> B.
4. Я даю вам стрелку h: Z -> M, которая делает диаграмму коммутирующей (... и эта стрелка однозначно определяетсявыборы, сделанные до сих пор).

Мы часто притворяемся, что есть категория Hask, в которой объекты являются конкретными (мономорфными) типами, а стрелки являются функциями Haskell соответствующего типа.Давайте посмотрим, как работает вышеприведенный протокол, и продемонстрируем, что * Haskell data Pair a b = P a b является продуктом на Hask.

1. Вы даете мне два объекта (типа), A = a и B = b.

2. Я должен создать объект (тип) и две стрелки (функции).Я выбираю M = Pair a b.Затем я должен написать функции типа Pair a b -> a (для стрелки fst: M -> A) и Pair a b -> b (для стрелки snd: M -> B).Я выбираю:

   fst :: Pair a b -> a
   fst (P a b) = a
   
   snd :: Pair a b -> b
   snd (P a b) = b
   

3. Вы даете мне объект (тип) Z = z и две стрелки (функции);f будет иметь тип z -> a, а g будет иметь тип z -> b.

4. Я должен создать функцию h типа z -> Pair a b.Я выбираю:

   h = \z -> P (f z) (g z)
   

   Это h требуется для переключения схемы.Это означает, что любые два пути через диаграмму, которые начинаются и заканчиваются в одном и том же объекте, должны быть равны.Для приведенных диаграмм это означает, что мы должны показать, что оно удовлетворяет двум уравнениям:

   f = fst . h
   g = snd . h
   

   Я докажу первое;второй аналогичен.

   fst . h
   = { definition of h }
   fst . (\z -> P (f z) (g z))
   = { definition of (.) }
   \v -> fst ((\z -> P (f z) (g z)) v)
   = { beta reduction }
   \v -> fst (P (f v) (g v))
   = { definition of fst }
   \v -> f v
   = { eta reduction }
   f
   

   По мере необходимости.

История для сопутствующих продуктов похожа, с небольшими изменениями в протоколе, описанном ниже:

1. Вы даете мне два объекта, A и B.
2. Я даю вам новый объект W, и две стрелки влево: A -> W и вправо: B -> W.
3. Вы даете мне объект Z и стрелки f: A -> Z и g: A -> Z.
4. Я даю вам стрелку h: W -> Z, которая делает диаграммы коммутирующими (...и эта стрелка однозначно определяется сделанными на данный момент решениями.)

Адаптировать приведенное выше обсуждение продуктов должно быть простым, и Pair, чтобы увидеть, как это будет применяться к побочным продуктам и data Copair a b = L a | R b.