Как неучтенные и фэннины связаны в теории категорий?

В библиотеке, которую я пишу, я считаю, что было бы элегантно писать класс, похожий на (но немного более общий) следующий, который объединяет как обычные uncurry над продуктами, так и fanin (от здесь или здесь, если вы предпочитаете):

{-# LANGUAGE TypeOperators, TypeFamilies,MultiParamTypeClasses, FlexibleInstances #-}
import Prelude hiding(uncurry)
import qualified Prelude 

class Uncurry t r where
    type t :->-> r
    uncurry :: (t :->-> r) -> t -> r

instance Uncurry () r where
    type () :->-> r = r
    uncurry = const

instance Uncurry (a,b) r where
    type (a,b) :->-> r = a -> b -> r
    uncurry = Prelude.uncurry

instance (Uncurry b c, Uncurry a c)=> Uncurry (Either a b) c where
    type Either a b :->-> c = (a :->-> c, b :->-> c)
    uncurry (f,g) = either (uncurry f) (uncurry g)

Обычно я просматриваю пакет Edward Kmett categories (связанный выше), чтобы понять мои вещи, но в этом пакете у нас есть фаны и недра, разделенные соответственно на классы CoCartesian и CCC.

Я немного читал о BiCCCs, но пока не понимаю их.

Мои вопросы

  • Является ли абстракция выше оправданной каким-то образом щуриться в теории категорий?

  • Если да, то каков был бы правильный язык, основанный на CT, чтобы говорить о классе и его экземплярах?

РЕДАКТИРОВАТЬ. В случае, если это поможет, и упрощение выше искажает вещи: в моем фактическом приложении я работаю с вложенными продуктами и копроизведениями, например. (1,(2,(3,()))). Вот реальный код (хотя по скучным причинам последний экземпляр упрощается и не работает отдельно, как написано)

instance Uncurry () r where
    type () :->-> r = r
    uncurry = const

instance (Uncurry bs r)=> Uncurry (a,bs) r where
    type (a,bs) :->-> r = a -> bs :->-> r
    uncurry f = Prelude.uncurry (uncurry . f)

-- Not quite correct
instance (Uncurry bs c, Uncurry a c)=> Uncurry (Either a bs) c where
    type Either a bs :->-> c = (a :->-> c, bs :->-> c)
    uncurry (f,fs) = either (uncurry f) (uncurry fs) -- or as Sassa NF points out:
                                                     -- uncurry (|||)

Итак, экземпляр const для экземпляра () пришел естественным образом как рекурсивный базовый случай для экземпляра n-ary tuple uncurry, но все три вместе выглядели как что-то не произвольное.

Обновление

Я обнаружил, что мышление в терминах алгебраических операций, a.la Chris Taylor блоги об "алгебре ADT" . Сделав это, я разъяснил, что мой класс и методы - это действительно законы экспоненты (и причина, почему мой последний пример был неправильным).

Вы можете увидеть результат в моем пакете shapely-data, в классах Exponent и Base; см. также источник заметок и разметку неаккуратного документа.

Ответы

Ответ 1

Ваш последний экземпляр Uncurry - это именно uncurry (|||), поэтому в нем нет ничего более общего.

Карри находит для любой стрелки f: A & times; B → C a curry f: A → C B так что уникальная стрелка eval: C B & times; B & C коммутирует. Вы можете просмотреть eval как ($). Высказывание "CCC" является сокращением для "в этой категории мы имеем все продукты, все экспоненты и терминальный объект" - другими словами, currying работает для любой пары типов и любой функции в haskell. Одним из важных следствий существования CCC является то, что A = 1 & times; A = A & times; 1 (или a изоморфно (a,()) и изоморфно ((),a)).

Нераспространение в haskell - это противоположная маркировка того же процесса. Начнем со стрелки f = uncurry g. Каждая пара имеет два проекции, поэтому композиция proj 1 и curry f= g дает C B. Поскольку мы говорим о составе и продуктах, неучтенное в CCC определяет уникальное uncurry g для любого g: A → C B. В CCC у нас есть все продукты, поэтому мы имеем C B & times; B, которые можно охарактеризовать на C.

В частности, вспомним A = A & times; 1. Это означает, что любая функция A → B также является функцией A & times; 1 → B. Вы также можете рассматривать это как "для любой функции A → B существует функция A & times; 1 → B", доказанная тривиальным неуправляемым, из которых ваш первый экземпляр делает только половину (это доказывает только для id).

Я бы не назвал последний экземпляр "неустранимым" в том же смысле, что и определение карри. Последний пример представляет собой конструкцию определения копродукта - для любой пары стрелок f: A → C и g: B → C имеется уникальная стрелка [f, g]: (A + B) → C. В этом смысле это выглядит как злоупотребление интерфейсом - это обобщение смысла от "неоткуда", чтобы "что-то дать, дать мне что-то" или "истинное соответствие между :->-> и функциями haskell". Возможно, вы можете переименовать класс в Arrow.