Hask类别中的值应该放在哪里？

Question

Hask类别中的值应该放在哪里？

haskellcategory-theory

28

所以我们有Hask范畴，其中：

类型是该范畴的对象
函数是从一个对象到另一个对象的态射。

类似地，对于Functor，我们有：

类型构造函数作为从一种范畴到另一种范畴的对象映射
fmap用于从一种范畴到另一种范畴的态射映射。

现在，当我们写程序时，我们基本上转换值（而不是类型），而且似乎Hask范畴根本不涉及值。我试图将值纳入整个方程式，并得出以下结论：

每个类型本身都是一个范畴。例如：Int是所有整数的范畴。
从一个值到同一类型的另一个值的函数是该范畴的态射。例如：Int -> Int
从一个值到另一个不同类型的值的函数是用于将一种类型的值映射到另一种类型的函子。

现在我的问题是 - 值在Hask范畴（或一般范畴理论）中是否有意义？如果是，则有何参考资料可供阅读；如果不是，则有何原因。

我希望问题说得清楚明白 :)

- Ankur

@AndrewC：所以在另一个层面上，类别中的每个对象本身都可以是类别？听起来就像是无限嵌套的类别 :) - Ankur

3

想要了解如何将整数视为一个范畴，可以阅读这篇维基学院文章：Introduction_to_Category_Theory/Monoids。或许这并不是一个“无底深渊”的范畴，但它可能是一个“无穹顶”的范畴！ - AndrewC

5个回答

14

正如我在安德鲁的回答中评论的（除此之外，这是非常好的），你可以把类型中的值看作该类型的对象，把函数看作函子。以下是两种完整的方式：

集合作为无聊的范畴

数学中最常用的工具之一是“等价类” - 即具有等价关系的集合。我们可以通过“群体”的概念以范畴论的方式来思考它。群体是一个范畴，其中每个态射都有一个反射，使得f . (inv f) = id和 (inv f) . f = id。

为什么这捕捉到了等价关系的想法？嗯，等价关系必须是自反的，但这只是它具有恒等箭头的范畴主张，它必须是传递的，但这只是组合，最后它需要是对称的（这就是我们添加反函数的原因）。

在任何集合上的数学中普通的等式概念因此产生了群体结构：即其中唯一的箭头是恒等箭头！这通常被称为“离散范畴”。

向读者留下练习的是，所有函数都是离散范畴之间的函子。

如果您认真考虑这个想法，就会开始思考具有不仅是恒等性的“相等性”的类型。这将允许我们编码“商类型”。此外，群体结构具有一些更多关于“相等证明的相等性”的公设（结合律等），这导致了n-群体和更高阶范畴论的道路。这很酷，尽管要使用它，您需要依赖类型和一些尚未完全解决的部分，当它最终进入编程语言时应该允许

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'))

在 JavaScript 中，Undefined 比其他值更不确定，因为它指的是没有终止的值（实际上，在 Haskell 中，undefined 函数在每个函数中都是通过抛出异常来实现的，但我们假装 undefined = undefined）。你无法确定某些值是否已经结束。如果给定一个未定义的值，您只能等待并查看。因此，它可能是任何东西。

部分顺序以标准方式产生一个范畴。

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

为什么函数是函子？嗯，函数无法知道它已经得到了一个未定义的值，因为这是停机问题。因此，它必须在遇到未定义值时返回一个未定义值，或者无论得到什么样的值都必须产生相同的答案。现在就由您来证明它确实是一个函子。

- Philip JF

11

尽管这里还有其他非常出色的答案，但它们都在某种程度上忽略了您的第一个问题。要明确的是，在Hask范畴中，值 根本不存在，并且没有意义。这不是Hask用来讨论的内容。

以上观点似乎有点愚蠢或感性，但我提出来是因为重要的是要注意，范畴论只提供了一种检查编程语言中复杂交互和结构的透镜。期望所有这些结构都被包含在范畴的相当简单的概念中是不可行的。[1]

换句话说，我们正在尝试分析一个复杂的系统，有时候将其视为一个范畴是有用的，以便寻找有趣的模式。正是这种思维方式让我们引入了Hask，检查它是否真的形成一个范畴，注意到Maybe似乎像一个函子，然后使用所有这些机制来写下一致性条件。

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中，对象是Haskell类型，箭头是在那些类型之间的Haskell函数。

让我们再看一下Maybe。如果它要成为Hask上的一个自函子，那么我们需要一种方法来将Hask中的所有类型映射到其他类型。这个映射不是一个Haskell函数，即使它可能感觉像一个： pure :: a -> Maybe a并不符合要求，因为它在值级别上操作。相反，我们的对象映射是Maybe本身：对于任何类型a，我们都可以形成类型Maybe a。

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

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

现在，很难不直接称呼Maybe [f]为“fmap f”，但在跳入这一步之前，我们可以再做些工作。Maybe [f]需要具备某些相容性条件。特别地，在Hask中的任何类型a都有一个id箭头。在我们的元语言中，我们可能称之为id [a]，我们也知道它还叫做Haskell名称id :: a -> a。总之，我们可以使用这些来陈述范畴自函子的相容性条件：

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

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

虽然上述内容相当技术性和复杂，但保持概念清晰并将Hask和范畴自函子的概念与它们的Haskell实例化分开，这一点非常重要。特别地，我们可以发现所有这些结构，而无需引入需要fmap作为真正的Haskell函数存在的需要。Hask是一个在值级别上不需要引入任何东西的范畴。

这就是将Hask视为范畴的真正核心所在。用Functor来标识Hask上的自函子需要更多的线条模糊。

这种线条模糊是有道理的，因为Hask具有指数。这是一种棘手的方式，即范畴箭头的整个捆绑和Hask中特定的、特殊的对象之间存在统一。

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

这很奇怪。

我最初声明一般的Haskell值在Hask的范畴呈现中根本没有表示。然后我接着演示了我们可以仅使用其范畴概念就可以做很多Hask的工作，而不必将这些部分实际放入Haskell中作为值。

现在我注意到像a -> b这样的类型的值实际上存在于元语言集合Hask (a, b)中的所有箭头中。这是一个很棒的技巧，正是这种元语言的模糊使得具有指数的范畴变得如此有趣。

不过，我们可以做得更好！Hask还有一个终端对象。我们可以通过元语言方式称之为0，但我们也知道它是Haskell类型()。如果我们查看任何Hask对象a，我们知道有一整套范畴箭头在Hask（()，a）中。进一步地，我们知道它们对应于类型() -> a的值。最后，因为我们知道给定任何函数f :: () -> a，我们可以通过应用()立即获得a，所以我们可能想说，在Hask（()，a）中的范畴箭头恰好是类型a的Haskell值。

这可能会非常令人困惑或者非常令人震惊。

我将以某种哲学的方式结束这个话题：Hask根本不讨论Haskell值。作为一个纯范畴，它实际上并没有讨论这些额外的类型、值和typeOf包含等范畴外概念，正是因为范畴非常简单，所以才有趣。

但我还是展示了即使作为一个严格的仅仅是一个范畴，Hask也具有类似于所有Haskell值的东西：对于每个Hask对象a，Hask（()，a）的箭头看起来非常相似。

从哲学上讲，我们可以认为这些箭头并不是我们正在寻找的Haskell值---它们只是替代品，范畴模拟。你可能会说它们是不同的东西，只是碰巧与Haskell值一一对应。

我认为这是一个非常重要的想法。这两件事情是不同的，但它们的行为非常相似。

非常相似。任何范畴都可以组合箭头，所以假设我们选择Hask（a，b）中的一些箭头和Hask（()，a）中的一些箭头。如果我们将这些箭头与范畴组合结合，我们得到Hask（()，b）中的一个箭头。稍微转变一下思路，我们可以说，我刚才找到了类型a -> b的值，类型a的值，然后将它们组合起来产生了类型b的值。

换句话说，如果我们侧面看事物，我们可以将范畴箭头组合看作函数应用的一般形式。

这就是使Hask等类别如此有趣的原因。广义上，这些类型的类别被称为笛卡尔闭类别或CCCs。由于拥有初始对象和指数（也需要乘积），它们具有完全模拟类型λ演算的结构。

但它们仍然没有值。

[1] 如果您在阅读我的答案之前阅读本文，则请继续阅读。事实证明，虽然期望发生这种情况是荒谬的，但实际上确实有点像。如果您是在阅读完整个答案后再阅读本文，则让我们反思一下CCC有多酷。

- J. Abrahamson

我一直听说 Fast and Loose 传达了这个粗略的想法，但我从未真正阅读过这篇论文，所以我不喜欢个人推荐它。 - J. Abrahamson

2

@JJJ 这里的核心和重要点是范畴论不涉及值；它的价值在于将值抽象出来。你可以使用函数恢复值，或者某些范畴具有集合作为对象，这些都不是主要的点。PhilipJF的回答很好地阐述了如何使用定义性将类型转换为范畴。AndrewC的回答澄清了一个类型作为范畴与Hask不同，处于不同的层次。这个答案是关于范畴论的基本教学要点。我将用完我的声望来奖励想要给予的赏金！ - not my job

1

在我看来，原问题的答案非常明确，即值在Haskell中的位置。Haskell值是从Hask中的终端对象出发的箭头，即对象的全局元素（那么范畴论不就是关于值的吗？;))，我们可以用a :: () -> A; a _ = ...; ... f[a()] ...替换任何a :: A; a = ...; ... f[a] ...在Haskell中，并将此a解释为Hask中的箭头1 -> A。通常，箭头不仅仅是函数，而是它们的等价类（通过外延相等性），因此给出相同值的两个函数() -> A是Hask中的同一箭头。 - JJJ

1

@JJJ 我所说的“符号技巧”是指类型中的值的概念和(::)通常并没有真正被范畴论所捕捉，尽管我们可以在Hask中看到它被编码了。看到这种编码与我们的价值/类型概念同构非常有趣，但如果您甚至在打破墙之前就抹去了这种区别，那么您已经将一个有趣的实现降低到了琐碎的程度。 - J. Abrahamson

3

@JJJ 是的，但你同样可以说类型就是集合，而且你的构造确实与元素同构，但范畴论的美和力量在于对象/态射抽象。从学习的角度来看，你需要暂时离开点并专注于对象、态射、函子、自然变换等方面，就像学习 Haskell 时需要暂时放下命令式思维，专注于函数、类型、多态性等方面一样。并不是说你不能做点（或状态），只是这不是主要的新思想。你从技术上是正确的。 - not my job

显示剩余9条评论

6

有几种将事物分类的方法，特别是编程语言，它们被证明是非常丰富的构造。

如果我们选择 Hask 类别，我们只是设置了一个抽象层次。这个层次不太适合谈论值。

然而，在 Hask 中可以将常量建模为从终端对象 () 到相应类型的箭头。例如：

- True : () -> Bool - 'a' : () -> Char 你可以查看：Barr，Wells -《计算机类别理论》，第2.2节。

- Euge

4

任何具有终端对象（或具有终端对象*）的范畴都有所谓的全局元素（或点，或常数，也可以在维基百科上找到更多信息，例如，在Awoday的范畴论书中，参见2.3广义元素），这些对象的全局元素我们可以称为这些对象的值，将全局元素作为“值”的自然和普遍的范畴概念。请注意，保留HTML标签。

例如，Set 具有通常元素 (集合、Set 对象) 作为全局元素，这意味着任何集合 A 的元素都可以被视为从不同函数 (即 Set 中的态射) {⋆} → A 到该集合 A 的单位集合 {⋆}。对于一个基数为 n 的有限集合 A，有 n 个这样的态射，对于空集合 {}，在 Set 中不存在这样的态射 {⋆} → {}，因此 {} “没有元素”，且 |{}| = 0；对于单元素集合 {⋆} ≊ {+} 唯一，因此 |{⋆}| = |{+}| = 1，等等。集合的元素或“值”实际上只是来自单元素集合 (1，在 Set 中是终对象) 的函数，因为在 Set 中存在一个同构 A ≊ Hom(1, A) (它是 CCC，因此 Hom 在此处是内部的，而 Hom(1, A) 是一个对象)。

因此，全局元素是将集合中元素的概念推广到具有终端对象的任何范畴的一般化。它可以通过广义元素进一步推广（在集合、偏序或空间范畴中，态射由对点的作用确定，但在一般范畴中并不总是这样）。通常，一旦我们将“值”（元素、点、常量、术语）转化为所讨论的范畴的箭头，我们就可以使用该特定范畴的语言来推理它们。

同样，在Hask中，例如，true为⊤ → Bool，而false为⊤ → Bool：

true :: () -> Bool
true = const True

false :: () -> Bool
false = const Frue

在通常的意义下，true ≠ false。此外，我们还有一个由⊥组成的家族，如⊤ → Bool（undefined，error "..."，fix，一般递归等等）。请注意保留HTML标签。

bottom1 :: () -> Bool
bottom1 = const undefined

bottom2 :: () -> Bool
bottom2 = const $ error "..."

bottom3 :: () -> Bool
bottom3 = const $ fix id

bottom4 :: () -> Bool
bottom4 = bottom4

bottom5 :: () -> Bool
bottom5 = const b where b = b

...

⊥ ≠ false ≠ true，这就是了，我们找不到其他形式的 ⊤ → Bool 的态射，因此 ⊥、false 和 true 是唯一可以在外延上区分的 Bool 值。请注意，在 Hask 中，任何对象都有值，即被占据，因为对于任何类型 A，总是存在形如 ⊤ → A 的态射，这使得 Hask 不同于 Set 或任何其他非平凡的 CCC（它的内部逻辑有点无聊，这就是《快速松散推理是道德上正确的》论文所讲述的内容，我们需要寻找一个具有良好逻辑的 CCC 的 Haskell 子集）。

此外，在类型理论中，值被语法地表示为项，这些项再次具有类别论语义。

如果我们谈论“纯粹的”（即完全的、BiCCC）Hask，那么这里是一个在Agda中证明A ≊ Hom(1, A)的简单证明（这很好地捕捉了纯粹的特点）。

module Values where

open import Function
open import Data.Unit
open import Data.Product
open import Relation.Binary.PropositionalEquality

_≊_ : Set → Set → Set
A ≊ B = ∃ λ (f : A → B) → ∃ λ (f⁻¹ : B → A) → f⁻¹ ∘ f ≡ id × f ∘ f⁻¹ ≡ id

iso : ∀ {A} → A ≊ (⊤ → A)
iso = const , flip _$_ tt , refl , refl

- JJJ

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- AndrewC · Accepted Answer

在范畴论中，一个重要的思想是将大而复杂的事物视为一个点。因此，当您考虑范畴Hask时，所有整数的集合/群/环/类/范畴被视为单个点。

同样，对于整数上的非常复杂的函数，它只被视为箭头/收集中的单个元素（点/箭头）。

范畴论中的第一步是忽略细节。所以，范畴Hask并不关心Int可以被认为是一个范畴-那是在不同的层次上。Int只是Hask中的一个点（对象）。

每个幺半群都是一个只有一个对象的范畴。让我们用这个。

你可以将整数作为一个具有单个对象的范畴，并且它的态射是像(+1)、(+2)、(subtract 4)这样的函数。任何幺半群都可以用与整数相同的方式构建一个单对象范畴。

如果您将整数作为以加法为运算的范畴，则从整数作为范畴到某个带有形成范畴的操作£的另一种类型中的函数f只能是一个函子，如果您拥有f(x+y)=f(x)£f(y) (这称为幺半同态)。大多数函数都不是态射。

字符串在++下构成一个幺半群，因此它们可以视为范畴。

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 不是一个态射，因为 quiteLong "Hello " 是 False，quiteLong "there!" 也是 False，但是 quiteLong ("Hello " ++ "there!") 是 True，而 False || False 不是 True。

因为 quiteLong 不是一个态射，所以它也不是一个函子。

你的观点是什么，Andrew？

我的观点是，一些 Haskell 类型可以被认为是范畴，但并不是所有它们之间的函数都是态射。

我们没有同时考虑不同层次的范畴（除非你在某种奇怪的目的下使用两个范畴），并且在对象和态射上故意没有理论交互，因为没有关于对象和态射的详细信息。

这部分是因为范畴论起源于数学领域，提供了一种语言来描述 Galois 理论中有限群/子群和域/扩张之间美妙的相互作用，这两个表面上完全不同的结构竟然紧密相关。后来，同调/同伦理论使拓扑空间和群之间的函子成为了有趣且有用的对象，但主要的一点是在一个函子的两个范畴中对象和态射允许非常不同。

（通常情况下，范畴论以从 Hask 到 Hask 的函子的形式出现在 Haskell 中，因此在实践中，函数编程中的两个范畴是相同的。）

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

每个类型本身都是一个范畴。例如，Int 是所有整数的一个范畴。

如果你以特定方式考虑它们的话。详见 PhilipJF 的回答。

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

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

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

不，不是所有函数都是函子，例如 quiteLong 不是。

值在 Hask 范畴（或一般的范畴论）中是否有意义？

范畴论中没有值，只有对象和态射，它们被视为