在类别理论中,如何与不相关和粉丝相关？

Question

在我正在编写的库中,我发现编写一个类似于(但略微更通用)以下类的类似乎是优雅的,它结合了通常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包(上面链接)来获取这类东西,但在那个包中我们分别将fanin和uncurry分成CoCartesian和CCC类.

我已经读过一些关于BiCCC的内容,但还没有真正了解它们.

我的问题是

1. 上面的抽象是否通过某种方式歪曲类别理论来证明？

2. 如果是这样,那么谈论类及其实例的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元元组uncurry实例的递归基本情况,但看到所有三个一起看起来像......非任意的东西.

---

更新

我发现在代数运算方面,a.la Chris Taylor 关于"ADT代数"的博客.这样做澄清了我的课程和方法实际上只是指数定律(以及我最后一个实例不正确的原因).

您可以在我的shapely-data包中Exponent和Base类中看到结果; 另请参阅注释的来源和非成功的doc标记.

Answer 1

你的最后一个Uncurry实例正是uncurry (|||)如此,所以没有什么"更普遍"的.

咖喱找到任何箭头f:A×B→C箭头咖喱_f:A→C ^B使得一个独特的箭头评估:C ^B ×B→C通勤.您可以将eval视为($).说"CCC"是"在这个类别中我们拥有所有产品,所有指数和终端对象"的简写 - 换句话说,curry适用于任何类型和haskell中的任何函数.成为CCC的一个重要结果是A = 1×A = A×1(或a与其同构(a,())并且同构((),a)).

haskell中的不合理是相同过程的标签.我们从箭头f = uncurry _g开始.每对具有两个突起,所以凸出的组合物₁和咖喱_˚F =克给出Ç ^乙.因为我们正在谈论的组合物和产品,在CCC uncurrying定义了唯一的uncurry _克任何克:A→C ^乙.在CCC我们有所有产品,所以我们有C ^B ×B,可以推广到C.

特别是,召回A = A×1.这意味着任何函数A→B也是函数A×1→B.您还可以将其视为"对于任何函数A→B,有一个函数A×1→B",通过无关紧要的证据证明,其中您的第一个实例只有一半(仅证明了这一点id).

我不会将最后一个实例称为"不合理",就像定义currying一样.最后一个例子是联产品定义的结构 - 对于任何一对箭头f:A→C和g:B→C,有一个独特的箭头[f,g] :( A + B)→C.从这个意义上来说,它似乎是对界面的滥用 - 它是意义的概括,从"不合理"到"给予某些东西,给我一些东西"或"真正的对应关系:->->和哈斯克尔函数".也许,您可以将类重命名为Arrow.