lambda - 编程中Category的类比是什么

Question

我发现逻辑和编程之间存在同构，称为Curry-Howard 对应关系，那么类别理论是否存在这样的等价关系，有助于理解 Functors 或 Monads 之类的东西？

Answer 1

是的！它被称为Curry-Howard-Lambek - 它将 Category 对象映射到类型，将态射映射到术语。因此，类型化的 lambda（没有名称的函数）甚至函数可以表示为笛卡尔封闭的类别，其中 Unite-type 成为终端对象，类型集（或更复杂的结构）是product，而 apply+currying 是指数。