Haskell"id"函数必须返回与传入的值相同的要求的类别 - 理论基础是什么？

Question

以下都是如此？

1. 在Hask类别中,Objects是Haskell类型,而Morphisms是Haskell函数.价值观不起作用Hask.
2. 身份态射被定义为源自对象A并终止于同一对象的箭头A.
3. 身份态射的作用由Haskell id函数扮演.
4. 从Haskell id函数返回的值必须与传入的参数值相同.

如果在类别理论中将身份态射定义为从对象A返回到相同对象A的箭头,那么类型的任何和每个Haskell函数都不满足该描述f :: A -> A吗？

还有一个问题,其答案可能也可能涵盖这一主题,但他们似乎对类别理论有一定程度的熟悉,而我很遗憾不具备这种理论.

在我看来,这是一个非常基本的初级问题.那么有人可以仅使用初学者可以理解的语言,符号和名义构造来提供答案吗？

Answer 1

我不确定我是否真的理解你的问题.

但类别中的身份必须满足

id . f = f
g . id = g

对于任何f,g正确的类型.所以id不只是任何随机函数A -> A,它是满足上述要求的函数.

请注意,在Hask中,我们可以获得任何值 a :: A

id . (const a) = const a

于是

id (const a ()) = const a ()

于是

id a = a

那么id真的是我们所期望的.

Answer 2

id应该是任何给定的Haskell类型的身份态射.Hask中类型A的标识态射是类型的函数A -> A,但它不仅仅是类型的任何函数A -> A; 它必须遵守类别法.

特别是,它必须是具有向/从对象A的态射的合成的左右标识.如果idA是对象A 的识别态射,这意味着对于任何对象B和态射f :: A -> B,f . idA必须完全相同f,并且对于任何对象C和态射g :: C -> A,都ifA . g必须完全相同g.

我们可以A -> A通过挑选具体案例来测试您的声明,即任何类型的函数都可以是A的身份.让我们将take (+1) :: Integer -> Integer作为Integer的标识,并考虑该函数(*2) :: Integer -> Integer.现在很明显(*2) . (+1),(+1) . (*2)而且(*2)都是一样的,所以我们已经证明了 - 哦等等,这些功能完全不同.

注意我没有在这里引入Haskell值的相等性.我在谈论Hask类别中态射的平等性; 态射的平等当然属于范畴论的范畴,因为没有它,关于身份态射的范畴规律是没有意义的.

我是在一个点上感到困惑的一个关键点是,虽然它没有意义考虑两个不同的对象与同类型(因为对象是,当我们谈论类型Hask),你可以有两个不同的态射具有相同的类型.类别理论确实允许在两个对象A和B之间存在几个不同的态射(并且允许从对象到自身的态射,这些态射不是同一性态,并且彼此区分).态射不是纯粹由他们的"端点"定义的.

身份法则实际上是非常严格的要求,并且应该强烈暗示不仅任何旧A -> A功能都会做idA.有一个明确的直觉,即能够在不改变它们的情况下与任意其他态射合成,身份态射需要"无所作为"(无论对于所讨论的类别意味着什么).

在Hask,我们知道态射是函数,对"无所事事"有一个非常明显的解释; 只返回其输入的函数.应该清楚的是,这确实适用于类别法:

f . id = f
id . f = f

还有,如果拟议的身份是射做任何事情等以后返回其输入不变(存在一些x这样badId x是不是x),那么你可以尝试与撰写反驳类别的法律id!

(badId . id) x
badId (id x)
badId x

badId x不是x,假设,badId . id不能等于id(由定义id x = x).所以badId不是作品的左侧身份.