前段时间我读到函数类型a -> b对应于关系a ≤ b，或者是a ≥ b吗？这对我来说很有意义，因为如果我们在它们之间存在双射（即(a ≈ b) ≡ (a -> b, b -> a)），则两种类型是同构的。同样，(a = b) ≡ (a ≤ b) ∧ (a ≥ b)。
我知道这不是 Curry-Howard-Lambek 对应（即类型论、逻辑和范畴论之间的对应）。这是类型论和其他东西之间的对应关系。我想了解更多有关此通信的信息。有人能指出我正确的方向吗？
我知道这似乎不是一个编程问题，但它与编程有关，我希望一些函数式程序员对此有更多了解，并能指出我正确的方向。
每个预购集形成一个类别。让我们(S, «)成为一个预先订购的集合。定义一个类别C，其对象是 if 的元素，并且 if 存在S，Hom(a, b)否则不存在。以您可能的唯一方式定义构图。范畴法则紧随前序的传递性和自反性。(a, b)a « b
特别是一个格，将形成一个允许有限积和联积的范畴。有界晶格将与初始对象和最终对象形成一个。
行为良好的函数式语言中的类型和函数也形成了一个具有有限积和联积以及初始和最终对象的类别。因此，如果你眯着眼睛看分类模糊，这些东西会开始看起来有点相似。
（这更像是一个评论而不是一个答案，但我需要更多的空间。）
类型a -> b对应a <= b。这很有用，例如，在类型级别谈论固定点，这是正确定义递归类型（列表、树等）所必需的。
回想一下递归是如何解决的，没有类别。在域论中，给定一个函数，f :: a -> a我们寻找一个最不x令人满意的f x = x（最不固定点）。事实证明，这也是最不x令人满意的f x <= x（最少前缀点）。然后我们得到归纳原理
f y <= y ==> fix f <= y
这基本上表明，如果我们有任何前缀点y，那么最小（预先）固定点fix f必须小于y- 实际上，它是最小的！
现在，让我们在上面撒一些类别粉末。蕴涵变成了->箭头，<=也变成了->。我们得到
(f y -> y) -> fix f -> y
似曾相识，我在哪里看到的……？啊!
newtype Fix f = Fix { unFix :: f (Fix f) }
cata :: Functor f => (f y -> y) -> Fix f -> y
cata g = g . fmap (cata g) . unFix
因此，cata一般消除器/变态只是旧归纳原理的类别授权版本。
请注意域点y现在如何成为我们类别中的对象（即类型）。此外，函数f必须适用于y，因此这些不是我们类别中的态射（可能是函数值 :: A -> B，从某种类型到某种类型），而是对应于类型类别中的函子（将类型映射到类型:: * -> *）。