26

所以我们有 Hask 的类别,其中:

  • 类型是类别的对象
  • 函数是范畴内对象到对象的态射。

同样,Functor我们有:

  • 类型构造函数作为对象从一个类别到另一个类别的映射
  • fmap用于将态射从一个类别映射到另一个类别。

现在,当我们编写程序时,我们基本上是转换值(而不是类型),而 Hask 的 Category 似乎根本不讨论值。我试图在整个方程中拟合值并得出以下观察结果:

  • 每个类型本身就是一个类别。例如:Int 是所有整数的范畴。
  • 从一个值到另一个相同类型的值的函数是范畴的态射。例如:Int -> Int
  • 从一个值到另一个不同类型的值的函数是将一种类型的值映射到另一种类型的函子。

现在我的问题是 - 值在 Hask 类别(或一般类别理论)中是否有意义?如果是,那么任何参考阅读它或者如果不是,那么任何原因。

我希望这个问题有意义:)

4

5 回答 5

26

(我将使用具有数学/类别理论而不是编程含义的单词,除非我mark it as code。)

一次一个类别

范畴论的一个重要思想是将大型复杂事物视为一个点,因此,当您考虑 Hask 范畴时,真正形成所有整数的集合/组/环/类/类别被认为是一个点.

同样,您可以对整数有一个非常复杂的函数,但它只是被认为是态射集合(集合/类)的单个元素(点/箭头)。

你在范畴论中做的第一件事就是忽略细节。所以类别 Hask 并不关心 Int 是否可以被视为一个类别 - 那是在不同的级别。Int 只是 Hask 中的一个点(对象)。

下一层

每个幺半群都是一个具有一个对象的类别。让我们使用它。

整数如何成为一个类别?

对此有不止一个答案(因为整数是加法下的幺半群和乘法下的幺半群)。让我们做加法:

您可以将整数视为具有单个对象的类别,而态射是诸如(+1),(+2),(减4)之类的函数。

您必须牢记我将整数 7 视为数字 7,但使用表示 (+7) 使其看起来像是一个类别。范畴论的定律故意说你的态射必须是函数,但如果某物具有一组包含恒等元且在合成下封闭的函数的结构,则它是一个范畴更清楚。

任何幺半群都以与我们刚刚处理整数相同的方式创建单个对象类别。

来自整数的函子?

一个函数f从整数作为一个类别下的运算+,到某个其他类型的运算£,形成一个类别,如果你有的话,只能是函子f(x+y) = f(x) £ f(y)。(这称为幺半群同态)。大多数函数不是态射。

示例态射

Strings 是 下的幺半群++,所以它们是一个类别。

len :: String -> Int
len = length

len是从Stringto的幺半群态射Int,因为len (xs ++ ys) = len xs + len ys, 所以如果你考虑 ( String, ++) 和 ( Int, +) 作为范畴,len是函子。

示例非态射

( Bool, ||) 是一个幺半群,以False为标识,所以它是一个单对象类别。功能

quiteLong :: String -> Bool
quiteLong xs = length xs > 10

is 不是态射,因为quiteLong "Hello "isFalsequiteLong "there!"is also False,但是quiteLong ("Hello " ++ "there!")isTrueFalse || Falseis not True

因为quiteLong不是态射,所以也不是函子。

你的意思是什么,安德鲁?

我的观点是,一些Haskell 类型可以被视为类别,但并非它们之间的所有函数都是态射。

我们不会同时考虑不同级别的类别(除非您出于某种奇怪的目的同时使用这两个类别),并且故意在级别之间没有理论上的相互作用,因为故意没有关于对象和态射的细节。

这部分是因为范畴论在数学中兴起,它提供了一种语言来描述伽罗瓦理论在有限群/子群和域/域扩展之间的可爱相互作用,这两个显然完全不同的结构,结果却是密切相关的。后来,同调/同伦理论使拓扑空间和群之间的函子变得既有趣又有用,但重点是在函子的两个类别中,对象和态射被允许彼此非常不同.

(通常范畴论以从 Hask 到 Hask 的函子形式进入 Haskell,因此在函数式编程的实践中,这两个范畴是相同的。)

那么......原始问题的答案到底是什么?

  • 每个类型本身就是一个类别。例如:Int 是所有整数的范畴。

如果您以特定的方式考虑它们。有关详细信息,请参阅 PhilipJF 的答案。

  • 从一个值到另一个相同类型的值的函数是范畴的态射。例如:Int -> Int

我认为你混淆了这两个层次。Hask中的函数可以是态射,但并不是所有的函数Int -> Int都是加法结构下的函子,例如f x = 2 * x + 10不是Int和Int之间的函子,所以它不是从( Int, +)到(的范畴态射(函子的另一种说法) Int+) 但它是Int -> IntHask 范畴中的态射。

  • 从一个值到另一个不同类型的值的函数是将一种类型的值映射到另一种类型的函子。

不,并非所有函数都是函子,例如quiteLong不是。

值在 Hask 类别(或一般类别理论)中是否有意义?

类别在类别理论中没有值,它们只有对象和态射,它们被视为顶点和有向边。对象不必具有值,并且值不是范畴论的一部分。

于 2013-06-29T14:05:27.067 回答
14

正如我评论 Andrew 的回答(否则非常好),您可以将类型中的值视为该类型的对象作为类别,并将函数视为函子。为了完整起见,这里有两种方法:

设置为无聊的类别

数学中最常用的工具之一是“setoid”——即一个具有等价关系的集合。我们可以通过“groupoid”的概念来明确地考虑这一点。群样是一个类别,其中每个态射都有一个逆,使得f . (inv f) = id(inv f) . f = id

为什么这抓住了等价关系的概念?好吧,等价关系必须是自反的,但这只是它具有恒等箭头的明确声明,并且它必须是传递的,但这只是组合,最后它需要是对称的(这就是我们添加逆向的原因)。

因此,数学中任何集合上的普通相等概念产生了一个群结构:即唯一的箭头是恒等箭头的结构!这通常被称为“离散类别”。

它留给读者作为练习,以表明所有函数都是离散类别之间的函子。

如果您认真对待这个想法,您就会开始怀疑具有“等式”的类型,而不仅仅是身份。这将允许我们对“商类型”进行编码。更重要的是,groupoid 结构还有一些公理(关联性等),这些公理是关于“等式证明的相等性”的主张,这导致了 n-groupoids 和更高范畴理论的道路。这是很酷的东西,虽然为了有用,你需要依赖类型和一些没有完全解决的位,当它最终进入编程语言时应该允许

data Rational where
    Frac :: Integer -> Integer -> Rational
    SameRationa :: (a*d) ~ (b*c) -> (Frac a b) ~ (Frac c d)

这样,每次您进行模式匹配时,您还必须匹配额外的相等公理,从而证明您的函数尊重等价关系,Rational 但不要担心这一点。只是“离散类别”的解释是一个非常好的解释。

指称方法

Haskell 中的每种类型都有一个额外的值,即undefined. 这是怎么回事?好吧,我们可以在每种类型上定义一个与值如何“定义”相关的偏序,这样

forall a. undefined <= a

但也像

forall a a' b b'. (a <= a') /\ (b <= b') -> ((a,b) <= (a',b'))

Undefined 的定义较少,因为它指的是不会终止的值(实际上,该undefined函数是通过在每个 haskell 中抛出异常来实现的,但我们假设它是undefined = undefined。你不能确定某些东西不会终止。如果你是给定一个undefined你所能做的就是等待和观察。因此,它可以是任何东西。

偏序以标准方式产生类别。

因此,每种类型都会产生一个类别,其中值以这种方式是对象。

为什么函数是函子?好吧,由于停止问题,函数无法告诉它已经得到了。undefined因此,它要么undefined在遇到 an 时返回 an,要么无论给出什么都必须产生相同的答案。由你来证明它确实是一个函子。

于 2013-06-29T18:05:46.600 回答
11

虽然这里还有其他一些非常棒的答案,但它们都有些想念你的第一个问题。需要明确的是,值在 Hask 类别中根本不存在并且没有任何意义。这不是 Hask 要谈论的。

上面说起来或感觉起来似乎有点愚蠢,但我提出来是因为重要的是要注意范畴论只提供了一个镜头来检查像编程语言这样复杂的东西中可用的更复杂的交互和结构。期望所有这些结构都包含在一个相当简单的类别概念中是没有成果的。[1]

另一种说法是,我们正在尝试分析一个复杂的系统,有时将其视为一个类别以寻找有趣的模式很有用。正是这种心态让我们引入了 Hask,检查它是否真的形成了一个类别,注意它Maybe的行为似乎像一个 Functor,然后使用所有这些机制来写下一致性条件。

fmap id = id
fmap f . fmap g = fmap (f . g)

无论我们是否引入 Hask,这些规则都是有意义的,但是通过它们视为简单结构的简单结果,我们可以在 Haskell 中发现,我们理解它们的重要性。


作为技术说明,这个答案的全部假设 Hask 实际上是“柏拉图式”Hask,即我们可以尽可能地忽略底部(undefined和非终止)。没有这一点,几乎整个论点都会分崩离析。


让我们更仔细地研究一下这些定律,因为它们似乎几乎与我最初的陈述背道而驰——它们显然是在价值层面上运作的,但是“在 Hask 中不存在价值”,对吧?

嗯,一个答案是仔细看看什么是分类函子。明确地说,它是两个类别(例如 C 和 D)之间的映射,它将 C 的对象映射到 D 的对象,并将 C 的箭头映射到 D 的箭头。值得注意的是,通常这些“映射”不是分类箭头——它们只是形成类别之间的关系,不一定与类别共享结构。

这很重要,因为即使考虑到 Haskell Functors,Hask 中的 endofunctors,我们也必须小心。在 Hask 中,对象是 Haskell类型,箭头是这些类型之间的 Haskell函数

让我们再看看Maybe。如果它将成为 Hask 上的 endofunctor,那么我们需要一种方法将 Hask 中的所有类型转换为 Hask 中的其他类型。这个映射不是一个 Haskell 函数,尽管它可能感觉像一个:pure :: a -> Maybe a不符合条件,因为它在级别上运行。相反,我们的对象映射Maybe本身就是:对于任何类型a,我们都可以形成 type Maybe a

这已经突出了在没有值的情况下在 Hask 中工作的价值——我们确实想要隔离一个Functor不依赖于pure.

我们将Functor通过检查我们的内函子的箭头映射来开发其余部分Maybe。这里我们需要一种将 Hask 的箭头映射到 Hask 的箭头的方法。现在让我们假设这不是一个 Haskell 函数——它不一定是——所以为了强调它,我们将用不同的方式编写它。如果f是 Haskell 函数a -> b,那么 Maybe[ f] 是其他一些 Haskell 函数Maybe a -> Maybe b

现在,很难不跳过并开始调用 Maybe[ f] " fmap f",但是在跳转之前我们可以做更多的工作。Maybe[ f] 需要有一定的连贯条件。特别是,对于aHask 中的任何类型,我们都有一个 id 箭头。在我们的元语言中,我们可能称它为 id[ a],而且我们碰巧知道它也使用 Haskell 名称id :: a -> a。总之,我们可以使用这些来说明内函子相干条件:

对于 Hask 中的所有对象a,我们有 Maybe[id[ a]] = id[ Maybe a]。对于 Haskf和中的任意两个箭头g,我们有 Maybe[ f . g] = Maybe[ f] 。也许[ g]。

最后一步是注意到 Maybe[_] 恰好可以作为 Haskell 函数本身作为 Hask 对象的值来实现forall a b . (a -> b) -> (Maybe a -> Maybe b)。这给了我们Functor


虽然上述内容相当技术性和复杂性,但重要的一点是保持 Hask 和分类内函子的概念直截了当,并与它们的 Haskell 实例化分开。特别是,我们可以发现所有这些结构,而无需引入fmap作为真正的 Haskell 函数存在的需要。Hask 是一个在价值层面根本没有引入任何东西的类别。

这就是将 Hask 视为一个类别的真正核心所在。在 Hask 上识别 endofunctors 的符号Functor需要更多的线模糊。

这种线模糊是合理的,因为Hask具有指数。这是一种棘手的说法,即整束分类箭头与 Hask 中特定的特殊对象之间存在统一。

更明确地说,我们知道对于 Hask 的任何两个对象,比如说ab,我们可以讨论这两个对象之间的箭头,通常表示为 Hask( a, b)。这只是一个数学集合,但我们知道 Hask 中还有另一种类型与 Hask( a, b) 密切相关:(a -> b)

所以这很奇怪。

我最初声明一般的 Haskell 值在 Hask 的分类表示中绝对没有代表。然后我继续证明我们可以用 Hask 做很多事情,使用它的分类概念,而不是将这些部分作为值实际粘贴到 Haskell 中。

但是现在我注意到,像这样的类型的值a -> b实际上确实作为元语言集 Hask( a, b) 中的所有箭头存在。这是一个相当巧妙的技巧,正是这种元语言模糊使得具有指数的类别如此有趣。

不过,我们可以做得更好一点!Hask 也有一个终端对象。我们可以通过将其称为 0 来从元语言学上谈论它,但我们也将其称为 Haskell 类型()。如果我们查看任何 Hask 对象,我们就会知道在 Hask( , )a中有一整套分类箭头。此外,我们知道这些对应于 type 的值。最后,由于我们知道给定任何函数,我们可以通过应用立即得到一个,因此可能想说 Hask( , ) 中的分类箭头正是Haskell类型的()a() -> af :: () -> aa()()aa

这应该要么完全令人困惑,要么令人难以置信。


我将坚持我最初的陈述,从哲学上结束这一点:Hask 根本不谈论 Haskell 价值观。它确实不是一个纯粹的类别——类别之所以有趣,正是因为它们非常简单,因此不需要所有这些额外的类型、值和typeOf包含等概念。

但我也(也许很糟糕)表明,即使作为一个严格的类别,Hask 也有一些看起来非常非常类似于 Haskell 的所有值的东西:每个 Hask 对象的 Hask( (), ) 的箭头。aa

从哲学上讲,我们可能会争辩说这些箭头并不是我们正在寻找的真正的 Haskell 值——它们只是替身,分类模拟。你可能会争辩说它们是不同的东西,只是碰巧与 Haskell 值一一对应。

我实际上认为这是一个非常重要的想法。这两件事是不同的,它们只是行为相似。


非常相似。任何类别都可以让您组合箭头,因此假设我们在 Hask( , ) 中选择了一些箭头,在 Hask( , a)b中选择了一些箭头。如果我们将这些箭头与类别组合结合起来,我们会在 Hask( , ) 中得到一个箭头。稍微把这一切放在头上,我们可能会说我刚刚做的是找到一个 type的值,一个 type 的值,然后将它们组合起来产生一个 type 的值。()a()ba -> bab

换句话说,如果我们从侧面看事物,我们可以将分类箭头组合视为函数应用的一种通用形式。

这就是让像 Hask 这样的类别如此有趣的原因。从广义上讲,这些类别称为笛卡尔封闭类别或 CCC。由于同时具有初始对象和指数(也需要乘积),它们具有完全模拟类型化 lambda 演算的结构。

但他们仍然没有价值

[1] 如果您在阅读我的其余答案之前阅读此内容,请继续阅读。事实证明,虽然期望这种情况发生是荒谬的,但它确实确实发生了。如果您在阅读了我的全部答案正在阅读本文,那么让我们反思一下 CCC 有多酷。

于 2014-01-30T16:29:54.077 回答
6

有几种方法可以将事物按照类别进行分类。特别是编程语言,结果证明是非常丰富的结构。

如果我们选择 Hask 类别,我们只是设置了一个抽象级别。一个不太舒服谈论价值观的水平。

但是,常量可以在 Hask 中建模为从终端对象 () 指向相应类型的箭头。然后,例如:

  • 真:()->布尔
  • 'a' : () -> 字符

您可以查看:Barr,Wells - Category Theory for Computing,第 2.2 节。

于 2013-11-16T06:27:24.283 回答
4
于 2014-01-31T16:56:02.747 回答