haskell - uncurry 和 fanin 在范畴论中是如何关联的？

Question

在我正在编写的库中，我发现编写一个与以下类似(但比其更通用)的类似乎很优雅，它结合了通常的 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 和 uncurry 分别分为 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 () 的实例instance 作为 n 元组 uncurry 实例的递归基本情况自然而然地出现，但是将这三个实例放在一起看起来像是……非任意的。

更新

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

您可以在我的 shapely-data 中查看结果包，在 Exponent and Base 类(class)；另请参阅注释和非古怪文档标记的来源。

Answer 1

您的最后一个 Uncurry 实例正是 uncurry (|||) ，所以没有什么“更笼统”的了。

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

Haskell 中的 Uncurry 是同一过程的相反标记。我们从箭头 f=uncurryg 开始。每对都有两个投影，所以 proj1 和 curryf=g 的组合给出了一个 CB。由于我们讨论的是成分和乘积，CCC 中的 uncurrying 为任何 g 定义了一个唯一的 uncurryg:A→CB。在 CCC 我们有所有产品，所以我们有 CB×B，可以评估为 C。

特别是，召回 A=A×1。这意味着任何函数 A→B 也是函数 A×1→B。您也可以将其视为“对于任何函数 A→B，都有一个函数 A×1→B”通过平凡的 uncurrying 证明，其中您的第一个实例只做了一半(仅证明 id )。

我不会把最后一个实例称为“uncurry”，就像定义柯里化(Currying)一样。最后一个例子是联积定义的构造——对于任何一对箭头 f:A→C 和 g:B→C，都有一个唯一的箭头 [f,g]:(A+B)→C。从这个意义上说，这似乎是对接口(interface)的滥用——它是从“uncurry”到“给定一些东西，给我一些东西”或“:->-> 和 haskell 函数之间的真正对应”的含义的概括。也许，您可以将类重命名为 Arrow。