【发布时间】：2015-01-03 06:37:43
【问题描述】：
我发现逻辑和编程之间存在同构，称为Curry-Howard correspondence，那么类别理论是否存在这样的等价物，有助于理解 Functor 或 Monads 之类的东西？
【问题讨论】：
标签： lambda functional-programming category-theory type-theory
【发布时间】：2015-01-03 06:37:43
【问题描述】：
是的！它被称为Curry–Howard–Lambek - 它将 Category 对象映射到类型，将态射映射到术语。因此，类型化的 lambda（没有名称的函数）甚至函数可以表示为 cartesian-closed category，其中 Unite-type 变为 terminal object，类型集（或更复杂的结构）为 product，apply+currying 为 @ 987654325@.
【讨论】：
-
据我了解，终端对象并不是真正的返回类型。它是具有从其他所有对象指向它的箭头的对象。任何类别中的终端对象在唯一同构之前也是唯一的，因此您可以说，在某种（重要）意义上，一个类别具有“只有一个”终端对象（如果它有一个）。在此类别中，终端对象是单元类型。这个关于初始对象和终止对象的视频非常好：youtube.com/watch?v=yeQcmxM2e5I
-
哦，我明白了，谢谢！我首先通过
Nothing(scala) 是终端，但后来意识到它是初始类型。所以封闭的范畴从假（Nothing）到真（Unit）。