库里霍华德的通信和平等

前段时间我读到函数类型a -> b对应的关系a ? b,或者是a ? b吗？这对我来说是有道理的,因为如果我们之间有双射(即(a ? b) ? (a -> b, b -> a))两种类型是同构的.同样地,(a = b) ? (a ? b) ? (a ? b).

我知道这不是Curry-Howard-Lambek的对应关系(即类型理论,逻辑和范畴理论之间的对应关系).它是类型理论与其他东西之间的对应关系.我想知道更多关于这种信件的信息.有人能指出我正确的方向吗？

我知道这似乎不是一个编程问题,但它与编程有关,我希望一些函数式程序员能够更多地了解它并指出我正确的方向.

每个预先订购的集合都形成一个类别.让我们(S, «)成为预先订购的套装.定义一个类别,C其对象是if 和无人居住的元素S和Hom(a, b)居住地.尽可能以唯一的方式定义构图.类别法立即遵循预订的传递性和反身性.(a, b)a « b

特别地,格子将形成允许有限产品和副产品的类别.有界格子将形成一个具有初始和最终对象的格子.

功能良好的函数式语言中的类型和函数也形成了一个包含有限产品和副产品以及初始和最终对象的类别.因此,如果你眯着眼睛看到一个明确的模糊,这些东西将开始看起来模糊地相似.