Haskell中的所有类型类都有类别理论模拟吗？

Question

考虑一个类型类,其成员类型* -> *.例如:Functor类型类.众所周知,在Haskell中,这种类型类与其数学(即类别理论)类似物之间存在对应关系.归纳:

问题1: Haskell中每个成员都是类型的每个类型类都* -> *对应于类别之间的某些功能吗？

现在考虑一个类型为类型的类型类*.例如,可以想象一个类型类Group对应于组的类别(从技术上讲,Group它将是Hask其对象包含所有Haskell类型的子类别).归纳:

问题2: Haskell中每个成员类型的类型类是否*对应于某个类别(技术上:某些子类别Hask)？

由此,可以问下一个一般性问题:

问题3:类型的类型是否等于或高于* -> * -> *某些类别理论概念？

实际上,整个问题可归纳如下:

一般问题:每个Haskell类型类都对应于某种类别的理论概念吗？

编辑:至少,似乎你可以说,因为每个类型类都包含一些Haskell类型作为其成员,你可以将每个类型类视为一些子类Hask(关闭.和利用id).

Answer 1

当充分迂腐地解释时,所有这些问题的答案都是"是",但是出于无意义的微不足道的原因.

每个类别C都限制为离散的子类别| C | 与C相同的对象,但只有身份态射(因此没有有趣的结构).至少,Haskell类型的操作可以被解释为离散类别上的操作|*|.最近的"角色"故事相当于(但不是旋转)试图承认态射是重要的,而不仅仅是物体.类型的"名义"角色相当于工作|*|而不是工作*.

(请注意,我不喜欢使用"Hask"作为"哈斯克尔类型和功能类别"的名字:我担心标注一种类别作为该哈斯克尔类别有致盲我们的财富不幸的副作用其他分类Haskell编程中的结构.这是一个陷阱.)

作为一个不同的迂腐,我注意到你可以把任何旧的废话作为任何旧类型的类型组合,没有任何有趣的结构(但具有微不足道的结构仍然可以断言,如果必须的话).但是,您在库中找到的类通常是结构丰富的.在类* -> *往往是由设计,的子类Functor,需要一定的自然变换的除存在fmap.

对于问题2.是的,当然一个课程*提供了一个子类别*.将对象从类别中删除是没有问题的,因为存在身份和复合的分类要求需要态射存在,给定对象,但不要求存在哪些对象.事实上它很有可能使它成为一个无聊的事实.然而,许多Haskell类型组合产生了*比那些仅作为子类别产生的类别更有趣的类别*.例如,Monoid该类为我们提供了一个类别,其中对象是实例,Monoid箭头是monoid homomorphisms:不仅是f从一个Monoid到另一个的任何旧函数,而是保留结构的一个:f mempty = mempty和f (mappend x y) = mappend (f x) (f y).

对于问题3,好吧,因为到处都是潜伏着大量的分类结构,当然有更多的分类结构可用(可能但不一定)更高级别.我特别喜欢索引族集之间的仿函数.

type (s :: k -> *) :-> (t :: k -> *) = forall x. s x -> t x

class FunctorIx (f :: (i -> *) -> (j -> *)) where
  mapIx :: (s :-> t) -> (f s :-> f t)

什么时候i和j重合,当这样f一个monad 时,问一下是明智的.通常的分类定义就足够了,即使我们已经* -> *落后了.

信息是这样的:没有任何关于成为类型类本身会引发有趣的分类结构; 有很多有趣的分类结构,可以通过各种类型的类型类来有效地呈现.从*(集合和函数)到* -> *(函子和自然变换),肯定有一些有趣的函子.不要被Haskell中关于"Hask"的丰富的分类结构的粗心大意所蒙蔽.

Answer 2

这里的问题之一是类别理论,也就是一般的抽象废话,是一种你可以用来谈论数学中几乎任何东西的理论.因此,我们所谈论的所有内容都可以使用类别理论的语言来表达,但我们可能不会产生任何有趣的结果.

Haskell中每个成员都是类型的每个类型类都* -> *对应于类别之间的某些函数吗？

不.这个问题包含类型错误!函数映射设置为集,但类别不是集.(换句话说,函数是类别Set中的态射.)类别是使用类来制定的,通常是适当的类,因此您不能将类别提供给函数.

我们将在* -> *Haskell类型的类别中调用morphisms中的对象.此类别的子类别是Haskell类型之间的仿函数类别,称为Functor.

Haskell中每个成员类型的类型类都*对应于某个类别(技术上:Hask的某个子类别)吗？

是.这是事实,但并不是非常有趣.只需从Hask中删除不在类型类中的每个对象,并删除Hask中不消耗的任何态射并从类型类中生成元素,并留下Hask的子类别.这个类别应该至少有一个对象?,和至少一个态射,id.

类型的类型是否等于或高于* -> * -> *某种类别的理论概念？

是.同样,这不会很有趣.我们来看一个X带类型的类型类* -> * -> *.

X类型类中的对象是否具有相同类型？嗯,是.但是这个类别不是很有趣,因为很难想象任何非平凡的态射.

X在某些类别中是态射吗？不,因为它无法组成.

是X一个算子,将Hask中类型的子类别映射到Hask中类型的态射的子类别？当然,但我们必须具备一定的专业知识,这两个X Y a b和X Z a b是允许的相同a b才允许进入态射我们对类型Hask的启动子类别.

在我看来,这似乎不会产生任何有用的见解,这并不奇怪,因为我们真的不知道任何事情X.

结论

类别理论是一种非常容易过度思考和过度使用的工具之一.如果您对类别理论本身并不感兴趣,我的建议是找到使用它的具体动机.特定的类型类(仿函数,透镜,monad,comonads等)有时会为您提供足够的结构或"原始数学材料",您可以从中构建类别理论中的有趣证明.但是对类型类的研究一般可能比它有用更抽象.