范畴论中，uncurry和fanin有什么关联？

Question

范畴论中，uncurry和fanin有什么关联？

13

在我编写的一个图书馆中，我发现编写一个类似于以下代码的类似物看起来非常优雅，它比通常的产品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 (|||)

因此，对于n元组的非柯里化实例，()实例的const实例自然而然地成为递归基本情况，但是看到所有三个实例在一起时，它们似乎是...某种非任意的东西。

更新

我发现，像Chris Taylor关于"ADT代数"的博客所说的那样，用代数运算的思路来考虑问题会更加清晰。这样做可以澄清我的类和方法实际上只是指数法则（也是为什么我的最后一个实例不正确的原因）。

你可以在我的shapely-data包中看到结果，其中包括Exponent和Base类；还可以查看源代码以获取注释和非奇怪的文档标记。

- jberryman

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- Sassa NF · Accepted Answer

您的最后一个 Uncurry 实例恰好是 uncurry (|||)，因此它没有任何“更一般”的内容。

Curry 为任何箭头 f：A×B→C 找到了一个箭头 curry_f：A→C^B，使得唯一的箭头 eval：C^B×B→C 具有可交换性。您可以将 eval 视为 ($)。说“CCC”是“在这个范畴中，我们拥有所有积、所有指数和一个终端对象”的缩写 - 换句话说，柯里化适用于 Haskell 中任何一对类型和任何函数。成为 CCC 的一个重要后果是 A=1×A=A×1 (或者 a 同构于 (a,()) 并同构于 ((),a))。

在 Haskell 中，Uncurry 是相同过程的相反标记。我们从箭头 f=uncurry_g 开始。每个对都有两个投影，所以 proj₁ 和 curry_f=g 的组合给出了 C^B。由于我们正在谈论组合和积，因此在 CCC 中 uncurrying 定义了任何 g：A→C^B 的唯一的 uncurry_g。在 CCC 中，我们拥有所有积，因此我们有 C^B×B，它可以 evaled 为 C。

特别地，回忆一下 A=A×1。这意味着任何函数 A→B 也是一个函数 A×1→B。您还可以将其视为“对于任何函数 A→B，都存在一个函数 A×1→B，通过简单的 uncurrying 得证，您的第一个实例只完成了一半（只证明了

id 的情况）。我不会像定义中的柯里化那样称最后一个实例为“非柯里化”。最后一个实例是对余积定义的一种构造。对于任何一对箭头f：A→C和g：B→C，都存在唯一的箭头[f，g]：（A+B）→C。从这个意义上讲，它似乎滥用了接口 - 它是从“非柯里化”到“给定某些内容，给我某些东西”或“:->->和Haskell函数之间的真正对应关系”的含义的概括。也许，您可以将类重命名为Arrow。