haskell - 类别理论中的非泛滥和fanin有何关系？

在我正在编写的库中，我发现写一个类似于以下内容(但比其稍微通用一些)的类看起来很优雅，该类将常用的uncurry和产品以及fanin函数(来自here，或here(如果您愿意):

{-# 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和uncurr分为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元元组uncurry实例的递归基例，但是看到这三个实例看起来就像……是任意的。

更新

我发现以a.la Chris Taylor的blogs about the "algebra of ADTs"代数运算的方式思考。这样做澄清了我的类和方法实际上只是指数定律(以及我的上一个实例不正确的原因)。

您可以在 shapely-data and Exponent 类的Base包中看到结果。另请参阅注释和非怪异文档标记的来源。

最佳答案

您的最后一个Uncurry实例正是uncurry (|||)，因此没有“更一般”的东西。

Curry为任何箭头f:A×B→C找到一个箭头curryf:A→CB，使得唯一的箭头eval:CB×B→C换向。您可以将eval视为($)。说“CCC”是“在此类别中，我们拥有所有产品，所有指数和一个终端对象”的简写-换句话说，curry适用于haskell中的任何类型对和任何函数。成为CCC的一个重要结果是A = 1×A = A×1(或者a与(a,())同构，而((),a)同构)。

haskell中的Uncurry是同一过程的相反标签。我们从箭头f = uncurryg开始。每对都有两个投影，因此proj1和curryf = g的组合给出CB。由于我们在谈论成分和产品，因此CCC中的uncurry为任何g定义了唯一的uncurryg:A→CB。在CCC中，我们拥有所有产品，因此我们拥有CB×B，可以将其逃避到C。

特别地，回想A ＝ A×1。这意味着任何函数A→B也是函数A×1→B。您也可以将其视为“对于任何功能A→B，都有一个功能A×1→B”，这是用平凡的琐事证明的，您的第一个实例仅做一半(仅针对id证明了这一点)。

我不会像定义currying一样将最后一个实例称为“uncurry”。最后一个例子是副产品定义的构建-对于任何一对箭头f:A→C和g:B→C，都有一个唯一的箭头[f，g] :( A + B)→C。从这个意义上讲，这似乎是对接口(interface)的滥用-它是对含义的泛化，从“无毛”到“给了东西，给我了东西”或“:->->和haskell函数之间的真正对应关系”。也许，您可以将类重命名为Arrow。

关于haskell - 类别理论中的非泛滥和fanin有何关系？，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/19262581/