Подтвердить что ты не робот

Какой категорический аналог для какой-то прикладной инфраструктуры я использовал?

Я читал немного о теоретической интерпретации категории Haskell. Аппликативные функторы: по-видимому, их можно интерпретировать в категориальных терминах как слабых замкнутых функторов или слабых моноидальных функторов (в зависимости от того, кого вы спросите, кажется), и это заставило меня задуматься о следующем.

Некоторое время назад я написал статью (вместе с Илья Сергеем и нашими советниками Фрэнком Писесеном и Дейвом Кларком) о примитиве рекурсии для "рекурсии эффекта" в DSL с использованием аппликативных функторов, предназначенных в основном для использования в библиотеках парсеров. Мы выяснили, что нам нужны несколько совершенно специальных конструкторов, которые кажутся похожими на них (как-то). Итак, я спрашиваю: некоторые из нижеприведенных конструкций каким-то образом связаны с теорией категорий, и если да, то как?

Заметим, что я напишу p ◦ q для композиции двух аппликативных функторов p и q.

Вот список необходимых нам примитивов:

  • afix: примитив рекурсии эффекта.  Нам действительно нужен примитив рекурсии, который выглядит так:

    afix :: (p a → p a) → p a
    

    Однако это было невозможно для более сложных интерпретаций p, которые нам нужны. Вместо этого мы получили следующее:

    afix :: (∀ q. Applicative q ⇒ p (q a) → p (q a)) → p a
    

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

  • Более глубже в реализации, нам нужен какой-то коапликационный оператор, который выглядит так:

    coapp0 :: (p a → p b) → p (a → b)
    

    Однако, требуя этого как общего оператора для p, похоже, он ограничил бы нас только тривиальными аппликативными функторами p. Вместо этого мы заметили, что можем выполнить следующие действия, которые можно реализовать:

    coapp :: Applicative p ⇒ (∀ q . Applicative q ⇒ (p ◦ q) a → (p ◦ q) b) → p (a → b)
    

Итак, вкратце: какое-либо из вышеизложенных как-то знакомое с категориальной точки зрения? В частности, ограничение по функциям типа ∀ q . Applicative q ⇒ (p ◦ q) a → (p ◦ q) b, а не p a -> p b, похоже, может быть фундаментальным каким-то образом? Есть ли какие-либо ссылки, которые могли бы помочь нам больше понять этот материал, чем мы могли сделать в прошлом?

В и о том, как мы ее использовали, в случае, если кто-то заинтересован.

4b9b3361