Hask 类别中的值在哪里？

Question

所以我们有 Hask 的类别，其中：

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

Functor 类似，我们有：

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

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

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

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

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

Answer 1

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

设置为无聊的类别

数学中最常用的工具之一是“setoid”，即具有等价关系的集合。我们可以通过“groupoid”的概念来明确地考虑这一点。 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 函数是通过在每个 haskell 中抛出异常来实现的，但我们假设它是undefined = undefined。你不能确定某些事情不会终止。如果给你一个undefined，你所能做的就是等待和观察。因此，它可能是任何东西。

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

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

为什么函数是函子？嗯，一个函数不知道因为停止问题它得到了undefined。因此，它要么在遇到undefined 时回馈undefined，要么无论给出什么都必须产生相同的答案。由你来证明它确实是一个函子。

Answer 2

任何带有终端对象（或带有终端对象*s*）的类别都有所谓的global elements（或points，或constants，也称为on Wikipedia , 更多可以找到，例如，在 Awoday 的 book 上的 Category Theory 中，请参阅 2.3 Generalized elements) 的对象，我们可以在此处调用此对象的 值，将全局元素作为“价值”的自然和普遍的范畴概念。

例如，Set 具有通常的元素（集合，Set 的对象）作为全局元素，这意味着任何集合 A 的元素都可以视为 different 函数（Set 的态射) {⋆} → A 从unit set {⋆} 到这个集合A。对于具有|A| = n 的有限集A 有n 这样的态射，对于一个空集{} 在Set 中没有这样的态射{⋆} → {}，因此{}“没有元素”和|{}| = 0，对于单例集 {⋆} ≊ {+} 是唯一的，所以 |{⋆}| = |{+}| = 1，等等。集合的元素或“值”实际上只是来自单例集合的函数（1，Set 中的终端对象），因为在Set 中存在同构A ≊ Hom(1, A)（即CCC，因此@ 987654353@ 在这里是内部的，Hom(1, A) 是一个对象）。

因此，全局元素是将Set 中的元素概念推广到具有终端对象的任何类别。它可以用generalized elements 进一步概括（在集合、偏序或空间的类别中，态射由点上的动作决定，但在一般类别中并非总是如此）。一般来说，一旦我们将“值”（元素、点、常量、术语）转换为相关类别的箭头，我们就可以使用该特定类别的 the language 来推断它们。

类似地，在Hask 中，我们有，例如，true 作为⊤ → Bool 和false 作为⊤ → Bool：

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

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

true ≠ false 在usual sence 中，另外，我们有一个⊥ 家族作为⊤ → Bool（undefined，error "..."，fix，一般递归等等）：

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（它内部逻辑有点无聊，这就是 Fast and Loose Reasoning is Morally Correct 论文的内容，我们需要寻找 Haskell 的一个子集，它有一个很好的 CCC 和一个健全的逻辑）。 p>

此外，在类型论中，值在语法上被表示为同样has 类似分类语义的术语。

---

如果我们谈论“柏拉图式”（即总计，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

Answer 3

虽然这里还有其他一些非常精彩的答案，但它们都有些遗漏了您的第一个问题。需要明确的是，值 根本不存在并且 在 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 types，箭头是这些类型之间的 Haskell functions。

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

这已经凸显了在没有价值的情况下使用 Hask 工作的价值——我们确实想要隔离一个不依赖于 pure 的 Functor 概念。

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

现在，很难不跳过并开始调用 Maybe[f] "fmap f"，但在跳转之前我们可以做更多的工作。也许[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] 。也许[g]。

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

---

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

这就是将 Hask 视为一个类别的真正核心所在。在 Hask 上用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) 正是 a 类型的 Haskell 值。

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

---

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

但我也（也许很糟糕）表明，即使作为一个严格的只是一个类别，Hask 也有一些看起来非常非常类似于 Haskell 的所有价值观的东西：Hask 的箭头（@ 987654381@, a) 对于每个 Hask 对象 a。

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

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

---

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

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

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

但它们仍然没有值。

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

Answer 4

有几种方法可以按照类别来分类。特别是编程语言，结果证明是非常丰富的结构。

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

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

• True : () -> Bool
• 'a' : () -> 字符

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

Answer 5

（除非我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 是从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 类型可以被视为类别，但并非它们之间的所有函数都是态射。

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

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

（通常类别理论以从 Hask 到 Hask 的函子形式进入 Haskell，因此在函数式编程的实践中，这两个类别是相同的。）

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

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

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

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

我认为您混淆了这两个级别。函数可以是 Hask 中的态射，但并非所有函数 Int -> Int 都是加法结构下的 Functor，例如 f x = 2 * x + 10 不是 Int 和 Int 之间的函子，因此它不是类别态射（函子的另一种说法）来自(Int,+) 到 (Int,+) 但它是 Hask 类别中的态射 Int -> Int。

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

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

值在 Hask 类别（或一般类别理论）中是否有意义？

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