13

在我正在编写的库中，我发现编写一个与以下类似（但比稍微更通用）的类似乎很优雅，它结合了通常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类中看到结果；另请参阅注释和非古怪文档标记的来源。

4

1 回答 1

10

您的最后一个 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 1和 curry f =g 的组合给出了 C B。由于我们谈论的是成分和产品，因此 CCC 中的 uncurrying 为任何 g 定义了一个唯一的 uncurry g： A→C B。在 CCC 中，我们拥有所有产品，因此我们有 C B ×B，可以评估为 C。

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

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

于 2013-10-09T09:15:59.110 回答