值在哪里适合Hask类别？

Question

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

• 类型是类别的对象
• 函数是类别中从一个对象到另一个对象的态射.

同样Functor我们有:

• 一个Type构造函数,用于将对象从一个类别映射到另一个类别
• fmap 用于将态射从一个类别映射到另一个类别.

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

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

现在我的问题是 - 在Hask类别(或一般类别理论)中,值是否有意义？如果是,那么任何关于它的参考或如果没有,那么任何原因.

我希望这个问题有道理:)

Answer 1

(除非我,否则我将使用数学/类别理论中的含义而不是编程mark it as code.)

一次一个类别

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

类似地,你可以在整数上有一个非常复杂的函数,但它只被认为是态射集合(集合/类)的单个元素(点/箭头).

你在类别理论中做的第一件事是忽略细节.所以类别Hask并不关心Int可以被认为是一个类别 - 它处于不同的级别.Int只是Hask中的一个点(对象).

一级下来

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

整数如何成为一个类别？

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

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

你必须坚持认为我将整数7视为数字7,但使用表示法(+7)使其看起来像是一个类别.类别理论的定律并不是说你的态射必须是函数,但如果它具有一组包含同一性并且在组合下封闭的函数的结构,那么它就更清楚了.

任何monoid都以与我们刚刚完成的整数相同的方式生成单个对象类别.

整数的函子？

f从整数作为操作下的类别的函数,到具有形成类别的操作的+其他类型£的函数,如果有的话,只能是函子f(x+y) = f(x) £ f(y).(这称为monoid同态).大多数函数都不是态射.

示例态射

Strings是一个幺半群++,所以它们是一个类别.

len :: String -> Int
len = length

len是从幺射String来Int,因为len (xs ++ ys) = len xs + len ys,所以如果你正在考虑(String,++)和(Int,+)类别,len是一个仿函数.

示例非态射

(Bool,||)是一个幺半群,False作为身份,因此它是一个对象类别.功能

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

不是一个态射,因为quiteLong "Hello "是False,quiteLong "there!"也是False,但是,quiteLong ("Hello " ++ "there!")是True,而False || False不是True.

因为quiteLong不是态射,它也不是算子.

安德鲁,你有什么意思？

我的观点是,一些 Haskell类型可以被认为是类别,但并不是它们之间的所有函数都是morhpisms.

我们不会同时考虑不同级别的类别(除非你将这两个类别用于某些奇怪的目的),并且这些级别之间故意没有理论上的相互作用,因为故意没有关于对象和态射的详细信息.

这部分是因为类别理论在数学中起飞,以提供一种语言来描述伽罗瓦理论在有限群/子群与场/场扩展之间的可爱互动,这两种结构显然完全不同,结果是密切相关的.后来,同源/同伦理论在拓扑空间和群体之间建立了仿函数,这些算子既有趣又有用,但主要的一点是物​​体和态射在两个类别的仿函数中被允许彼此非常不同. .

(通常类别理论以Hask到Hask的仿函数形式进入Haskell,因此在函数式编程的实践中,这两个类别是相同的.)

那么...原始问题的答案究竟是什么？

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

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

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

我认为你把这两个级别搞混了.功能可以在Hask态射,但并非所有的功能Int -> Int都加结构下函子,例如f x = 2 * x + 10是不是int和Int之间的函子,所以它不是一个类别射从((说仿函数的另一种方式)Int,+)到(Int,+)但它是Int -> IntHask类别中的态射.

• 从一个值到另一个不同类型的值的函数是用于将一种类型的值映射到另一种类型的函数.

不,并非所有功能都是仿函数,例如quiteLong不是.

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

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

Answer 2

当我评论Andrew的答案(其他方面非常好)时,您可以将类型中的值视为该类型的对象作为类别,并将函数视为仿函数.为了完整起见,有两种方法:

设置为无聊类别

数学中最常用的工具之一是"setoid" - 也就是说,与它有等价关系的集合.我们可以通过"groupoid"的概念明确地想到这一点.一个群体是一个类别,其中每个态射都有一个逆,使得f . (inv f) = id和(inv f) . f = id.

为什么这会捕捉到等价关系的概念？那么,一个等价关系必须是自反的,但是这仅仅是个绝对的要求,它有身份的箭,它必须是传递的,但是这仅仅是组成,最终它必须是对称的(这就是为什么我们增加了倒数).

因此,任何集合中数学上的平等的普通概念产生了一种群体结构:即唯一的箭头是身份箭头!这通常被称为"离散类别".

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

如果你认真对待这个想法,你会开始怀疑具有"平等"的类型,而不仅仅是身份.这将允许我们编码"商类型".更重要的是,广群结构具有一些公理(associativty等)是关于一条通往正胚和更高的范畴论之路"平等证明平等"的权利要求.这是很酷的东西,虽然是有用的,你需要依赖的类型和一些没有完全制定出位,当它终于使得它成为编程语言应该允许

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函数是通过在每个haskell中抛出异常来实现的,但是我们假装它是undefined = undefined.你不能确定某些东西不会终止.如果你是给予undefined你所能做的就是观望.因此,它可以是任何东西.

部分订单以标准方式产生类别.

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

函数函数为什么？好吧,一个函数不能说它undefined因为停止问题而得到了它.因此,它要么必须undefined在遇到它时给予回报,要么无论给出什么都必须产生相同的答案.由你来表明它真的是一个仿函数.

Answer 3

虽然这里还有其他一些非常精彩的答案,但他们都会错过你的第一个问题.要清楚,价值根本不存在,并且在Hask类别中没有意义.这不是哈斯克斯要谈的内容.

上面的说法或感觉似乎有些愚蠢,但我提出来是因为重要的是要注意,类别理论只提供一个镜头来检查更复杂的交互和结构,这些交互和结构可用于像编程语言那样复杂的东西.期望所有这种结构都被类别的相当简单的概念所包含在内并不富有成效.[1]

另一种说法是我们试图分析一个复杂的系统,有时将它视为一个类别以寻找有趣的模式是有用的.正是这种心态让我们介绍了Hask,检查它是否真的形成了一个类别,通知Maybe看起来像一个Functor,然后使用所有这些机制来记下一致性条件.

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

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

作为一个技术说明,这个答案的全部假设Hask实际上是"柏拉图式的"Hask,即我们可以undefined根据自己的喜好忽略底部(和非终止).如果没有这一点,几乎整个论点都会分崩离析.

让我们更仔细地研究这些定律,因为它们似乎几乎与我的初始陈述相反 - 它们显然在价值水平上运作,但"Hask中不存在值",对吧？

好吧,一个答案就是仔细研究一下分类函子是什么.明确地,它的两个类别(比如C和d)这需要的C的对象的C d的目的和箭头D的箭头值得注意的是,在一般的这些"映射" s为不明确的箭头-它们简单地形成之间的映射类别之间的关系,并不一定与类别共享结构.

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

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

这已经凸显了在没有值的情况下在Hask中工作的价值 - 我们确实希望找出一个Functor不依赖于它的概念pure.

我们将Functor通过检查Maybeendofunctor 的箭头映射来开发其余部分.在这里,我们需要一种方法将Hask的箭头映射到Hask的箭头.我们现在假设这不是一个Haskell函数 - 它不必如此强调它我们将以不同的方式编写它.如果f是Haskell函数,a -> b则Maybe [ f]是其他一些Haskell函数Maybe a -> Maybe b.

现在,很难不向前跳,只是开始调用Maybe [ f]" fmap f",但我们可以在进行跳转之前做更多的工作.也许[ f]需要有一定的连贯性条件.特别是,对于aHask中的任何类型,我们都有一个id箭头.在我们的元语言中,我们可能将其称为id [ a],而我们碰巧知道它也是Haskell的名字id :: a -> a.总而言之,我们可以使用这些来表明endofunctor的一致性条件:

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

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

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

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

这条线模糊是合理的,因为Hask有指数.这是一种狡猾的方式,说明整个分类箭头和Hask中的特殊对象之间存在统一.

为了更加明确,我们知道,Hask:任何两个对象,说a和b,我们可以谈论这两个物体之间的箭头,往往表示为Hask( ,).a b这仅仅是一个数学集合,但我们知道,有一个在Hask的另一种类型是密切相关的Hask( ,a):b (a -> b)!

所以这很奇怪.

我最初声明一般的Haskell值在Hask的分类表示中绝对没有任何表示.然后我继续演示我们可以通过仅使用其分类概念并且实际上不将这些部分作为值粘贴在Haskell内部来完成Hask .

但是现在我注意到类似a -> b实际存在的类型的值确实存在于金属语言集Hask(a,b)中的所有箭头.这是一个非常诡计,正是这种金属语言的模糊使得带有指数的类别如此有趣.

不过,我们可以做得更好!Hask还有一个终端对象.我们可以通过将其称为0来讨论这种语法,但我们也知道它是Haskell类型().如果我们查看任何Hask对象,a我们就知道Hask((),a)中有一整套分类箭头.此外,我们知道这些对应于类型的值() -> a.最后,因为我们知道给定任何函数f :: () -> a我们可以a通过应用立即得到()一个可能想要说Hask((),a)中的分类箭头正是类型的Haskell 值a.

哪个应该是完全混乱或令人难以置信的令人兴奋.

我将通过坚持我的初始陈述来在哲学上结束这一点:Hask根本不讨论Haskell值.它真的不是一个纯粹的类别 - 类别很有意思,因为它们非常简单,因此不需要所有这些类别和价值以及typeOf包含等的超分类概念.

但我也,或许很差,表明即使是作为stricly 只是一个类别,Hask有一些看起来非常,非常相似,所有的Haskell的值:Hask(的箭头(),a)每次Hask对象a.

哲学上,我们可能会说,这些箭头不是真的,我们正在寻找的哈斯克尔值---他们只是替身,分类嘲笑.你可能会争辩说它们是不同的东西,但恰好恰好与Haskell值一一对应.

我实际上认为这是一个非常重要的想法.这两件事情是不同的,他们只是表现得相似.

非常相似.任何类别允许您撰写的箭,所以让我们假设我们挑Hask(一些箭头a,b)和Hask(一些箭头(),a).如果我们将这些箭头与类别组合结合起来,我们在Hask((),b)中得到一个箭头.我们可以说我刚才所做的就是找到一个类型a -> b的值,类型的值a,然后将它们组合起来产生一个类型的值b.

换句话说,如果我们侧身看事物,我们可以看到分类箭头组合作为功能应用的一般形式.

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

但他们仍然没有价值观.

[1]如果您在阅读我的其余答案之前阅读此内容,请继续阅读.事实证明,虽然期望这种情况发生是荒谬的,但实际上确实如此.如果您在阅读完整个答案后阅读本文,那么让我们只考虑一下CCC的酷炫程度.

Answer 4

有几种方法可以根据类别进行处理.特别是编程语言,结果是非常丰富的结构.

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

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

• 是的:() - >布尔
• 'a':() - > Char

您可以查看:Barr,Wells - 计算类别理论,第2.2节.