究竟什么是类别?

zer*_*ing 9 haskell scala category-theory

我正在为程序员阅读分类理论,我无法弄清楚究竟是什么类别.

我们考虑一下这种Bool类型.是Bool一个类别和/ TrueFalse对象(居民)?

K. *_*uhr 14

你得到很多可能令人困惑的答案的一个原因是你的问题有点像问:"让我们考虑一个足球.足球是一个'游戏',黑色和白色的多边形是'棋子'吗?"

答案可能是@ arrowd的回答:"不,你把足球(Hask)的比赛与球(Bool)相混淆,而多边形(TrueFalse)并不重要." 或者,它可能是@ freestyle的回答:"是的,我们当然可以使用足球创建一个游戏并将一个玩家分配给黑色多边形而另一个玩家分配白色多边形,但规则是什么?" 或者,它可能是@Yuval Itzchakov的答案:"正式地,'游戏'是一个或多个玩家的集合,零件或多件,以及一套规则,等等等."

所以,让我再加上一个(非常长的)答案的混乱,但也许它会更直接地回答你的问题.

是的,但这是一个无聊的类别

我们不是谈论Haskell类型Bool,而是谈谈布尔逻辑的抽象概念以及布尔值true和false.我们可以用抽象值"true"和"false"作为对象形成一个类别吗?

答案肯定是肯定的.事实上,我们可以(无限地)形成许多这样的类别.我们需要做的就是解释"对象"是什么,"箭头"(有时称为态射)是什么,并确保它们遵守类别的正式数学规则.

这是一个类别:让"对象"为"真"和"假",并让两个"箭头":

true -> true
false -> false
Run Code Online (Sandbox Code Playgroud)

注意:不要将此->表示法与Haskell函数混淆.这些箭头并不"意味着"任何东西,它们只是对象之间的抽象连接.

现在,我知道这是一个类别,因为它包含两个标识箭头(从一个对象到它自身),并且它满足组合属性,基本上说如果我可以跟随两个箭头a -> b -> c,则必须有一个直接箭头a -> c表示它们的"组成".(同样,当我写a -> b -> c,我不是在这里谈论一个函数类型-这是连接抽象的箭头ab,然后bc.)反正,我没有足够的箭头太担心组成的这一类,因为我不同对象之间没有任何"路径".我将其称为"离散布尔"类别.我同意它几乎没用,就像基于足球多边形的游戏一样非常愚蠢.

是的,但它与布尔值无关

这是一个稍微有趣的类别.让对象为"true"和"false",并让箭头为上面的两个标识箭头加上:

false -> true
Run Code Online (Sandbox Code Playgroud)

这也是一个类别.它具有所有的身份箭头,并且它满足构图,因为忽略身份箭头,我可以遵循的唯一有趣的"路径"是从"假"到"真",并且没有其他地方可去,所以我仍然没有真的有足够的箭头来担心构图规则.

您可以在这里写下几个类别.看看你能找到一个.

不幸的是,最后两个类别与布尔逻辑的属性没有任何关系.这是真的,false -> true看起来有点像一个not操作,但后来我们怎么能解释false -> false或者true -> true,为什么不能true -> false在那里,太?

最终,我们可以很容易地将这些对象称为"foo"和"bar"或"A"和"B",甚至不打算给它们命名,这些类别也同样有效.因此,虽然从技术上讲这些是具有"true"和"false"作为对象的类别,但它们并没有捕获有关布尔逻辑的任何有趣内容.

快速旁边:多个箭头

我还没有提到的东西是类别可以包含多个不同的箭头两个物体之间,所以有可能是两个箭头从ab.为了区分它们,我可能会给它们起名称,例如:

u : a -> b
v : a -> b
Run Code Online (Sandbox Code Playgroud)

我甚至可以将箭头身份分开b:

w : b -> b      -- some non-identity arrow
Run Code Online (Sandbox Code Playgroud)

组合规则必须由所有不同的路径满足.所以,因为有一条路径u : a -> b和一条路径w : b -> b(即使它没有"去"其他地方),也必须有一个箭头来表示u后面跟着的w组成a -> b.它的值可能再次等于"u",或者可能是"v",或者它可能是其他箭头a -> b.描述一个类别的部分原因在于解释所有箭头如何构成并证明它们遵守类别法(单位法和联想法,但我们不要在这里担心这些法律).

有了这些知识,您可以创建无限数量的布尔类别,只需在任何地方添加更多箭头,并根据类别法则发明您应该如何编写的任何规则.

如果您使用更复杂的对象,则排序

这是一个更有趣的类别,它捕获了布尔逻辑的一些"含义".解释起来有点复杂,所以请耐心等待.

让对象成为具有零个或多个布尔变量的布尔表达式:

true
false
not x
x and y
(not (y or false)) and x
Run Code Online (Sandbox Code Playgroud)

我们会认为是"永远不变"的表达式是相同的对象,所以y or falsey是同一个对象,因为无论什么价值y,它们具有相同的布尔值.这意味着可以编写上面的最后一个表达式(not y) and x.

让箭头表示将零个或多个布尔变量设置为特定值的行为.我们将这些箭头标记为带有少量注释,因此箭头{x=false,y=true}表示设置两个变量的行为.我们假设设置按顺序应用,因此箭头{x=false,x=true}对表达式具有相同的效果{x=false},即使它们是不同的箭头.这意味着我们有箭头:

{x=false} : not x -> true
{x=true,y=true} : x and y -> true
Run Code Online (Sandbox Code Playgroud)

我们还有:

{x=false} : x and y -> false and y  -- or just "false", the same thing
Run Code Online (Sandbox Code Playgroud)

从技术上讲,标记的两个箭头{x=false}是不同的箭头.(它们不能是同一个箭头,因为它们是不同对象之间的箭头.)在类别理论中,如果它们具有相同的"含义"或"解释",就像这样使用相同的名称,这是非常常见的,就像这些那些.

我们将箭头的组合定义为在第一个箭头中应用设置序列然后应用第二个箭头的设置的行为,因此组成:

{x=false}: x or y -> y     and    {y=true} : y -> true
Run Code Online (Sandbox Code Playgroud)

是箭头:

{x=false,y=true}: x or y -> true
Run Code Online (Sandbox Code Playgroud)

这是一个类别.它为每个表达式都有标识箭头,包括不设置任何变量:

{} : true -> true
{} : not (x or y) and (u or v) -> not (x or y) and (u or v)
Run Code Online (Sandbox Code Playgroud)

它为每对箭头定义了构图,并且构图遵循单位和关联定律(再次,我们不要在此担心这个细节).

并且,它代表布尔逻辑的一个特定方面,特别是通过将布尔值替换为变量来计算布尔表达式的值的行为.

你看!一个函子!

它也有一个有趣的函子,我们称之为"否定".我不会解释这里的仿函数是什么.我只想说Negate通过以下方式将此类别映射到自身:

  • 将每个对象(布尔表达式)取为逻辑否定
  • 将每个箭头移动到表示相同变量替换的新箭头

那么,箭头:

{a=false} : (not a) and b -> b
Run Code Online (Sandbox Code Playgroud)

由Negate仿函数映射到:

{a=false} : not ((not a) and b) -> not b
Run Code Online (Sandbox Code Playgroud)

或者更简单地说,使用布尔逻辑的规则:

{a=false} : a or (not b) -> not b
Run Code Online (Sandbox Code Playgroud)

这是原始类别中的有效箭头.

该仿函数捕获了"否定布尔表达式"等同于"否定其最终结果"的想法,或者更一般地说,在否定表达式中替换变量的过程具有与对原始表达式相同的结构.也许这不是太令人兴奋,但这只是一个很长的Stack Overflow答案,而不是一本500页的分类理论教科书,对吗?

Bool作为该Hask类别的一部分

现在,让我们从谈论抽象布尔类别转到您的具体问题,BoolHaskell 类型是否是具有对象True和类别的类别False.

上面的答案仍然适用,只要这个Haskell类型可以用作布尔逻辑的模型.

但是,当人们谈论Haskell中的类别时,他们通常会谈论一个特定的类别Hask,其中:

  • 对象是类型(如Bool,Int等)
  • 箭头是Haskell函数(如f :: Int -> Double). 最后,Haskell语法和我们的抽象类别语法重合 - Haskell函数f可以被认为是从对象Int到对象的箭头Double.
  • 成分是规律的功能成分

如果我们谈论这个类别,那么你的问题的答案是:不,在Hask类别中,Bool是对象之一,箭头是Haskell函数,如:

id :: Bool -> Bool
not :: Bool -> Bool
(==0) :: Int -> Bool

foo :: Bool -> Int
foo b = if b then 10 else 15
Run Code Online (Sandbox Code Playgroud)

为了使事情变得更复杂,对象包括函数类型,因此Bool -> Bool也是对象之一.使用此对象的箭头的一个示例是:

and :: Bool -> (Bool -> Bool)
Run Code Online (Sandbox Code Playgroud)

这是从对象Bool到对象的箭头Bool -> Bool.

在这种情况下,TrueFalse没有类别的一部分.哈斯克尔值函数类型,就像sqrt或者length是类,因为他们是箭头的一部分,但是TrueFalse是非功能类型,所以我们只是把它们从定义的.

分类理论

请注意,最后一个类别,就像我们查看的第一个类别一样,与布尔逻辑完全无关,即使它Bool是其中一个对象.事实上,这一类,Bool并且Int看起来差不多的-他们只是两种类型,可以有箭头离开或进入它们,你永远不会知道,Bool是关于真假或Int代表整数,如果你只是看着这个Hask类别.

这是范畴理论的一个基本方面.您使用特定类别来研究某个系统的特定方面.无论Bool是类别还是类别的一部分都是一个模糊的问题.更好的问题是,"这个特殊方面Bool是我对可以表现为有用类别的东西感兴趣吗?"

我上面给出的类别大致对应于以下潜在有趣的方面Bool:

  • "离散布尔"类别表示Bool两个对象的简单数学集合,"true"和"false",没有其他有趣的特征.
  • "false - > true"类别表示布尔值的排序false < true,其中每个箭头表示运算符"<=".
  • 布尔表达式类别表示简单布尔表达式的评估模型.
  • Hask 表示函数的组合,其输入和输出类型可以是布尔类型或涉及布尔值和其他类型的函数类型.