类型级别的函子只是 Hask 的 2 类中的函子吗？答案

【问题标题】：Are type-level functors just functors in the 2-category of Hask?类型级别的函子只是 Hask 的 2 类中的函子吗？
【发布时间】：2015-01-08 15:08:28
【问题描述】：

据我了解，Hask范畴的典型解释是该范畴的对象是Haskell类型，而态射是Haskell函数。

这样解释：

{-# LANGUAGE DataKinds, TypeOperators, TypeFamilies #-}
data Nat = Z | S Nat

type family Map (f :: Nat -> Nat) (x :: [Nat]) :: [Nat] where
Map f '[] = '[]
Map f (x ': xs) = (f x) ': (Map f (xs))

我们可以将Z 解释为Hask 的单个对象子类别，将S a 解释为函子，将类别Z 映射到类别S Z，并将其映射到类别S(S Z)，等等……

那么，和一个类型级别的提升列表（例如），一个类型级别的仿函数（如Map）会成为Hask的2类仿函数吗？

【问题讨论】：

Hask 是其对象具有种类* 的类别，因此Z-as-only-object 不是子类别，因为它具有种类Nat。不过，您当然可以将Z 视为一个类别——但态射是什么？如果不存在非平凡的，它甚至可能不会使这个想法无效，但我什至不知道如何称呼这些态射。
除了恒等态射之外没有态射。

标签： haskell category-theory

【解决方案1】：

您可以在这里将Map 视为从对象是同类事物Nat 的类别到对象是同类事物[Nat] 的类别的提升箭头。但这不是函子，因为它没有提供将Nat 的对象提升到[Nat] 的对象的规范方法（并且有多种方法可以做到这一点）。

如果您有一个更通用的Map，它在值级别上镜像事物，将a -> b 类型的函数发送到[a] -> [b] 类型的函数，那么它将给出一个函子。

在任何情况下，2 类都不会进入这张图片。 2-categories 的工作方式是它们就像普通的类别，但它们本身也有箭头之间的映射，它们也以正确的方式组成。（而更高的类别又在这些单元格之间有地图等）。所以Hask 不是一开始就属于 2 类，因为我们的箭头之间没有特殊的映射。

旁注：虽然Hask 不是 2 类，但它确实会产生一个相关的，因为它是“自身丰富的”。在这个类别中，对象是“hask-enriched categories”。也就是说，其对象是任何你选择的类别，但其态射是 haskell 函数——hask 的子类别由 e.g. []、Maybe 等都适合这里，例如）。这个范畴的态射是这些 Hask 丰富范畴之间的函子。也就是说，它们将对象映射到对象，将对象之间的（haskell）函数映射到对象之间的（haskell）函数。所以这些对应于我们通常认为的函子之间的自然转换。现在我们需要在那些之间添加真正的 2 细胞自然转换！也就是说，它们由我们认为的典型 Haskell 中的“自然变换的态射”组成。

但这并不是我想象的你的想法。

【讨论】：