编程中类别的类比是什么？

问题描述

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

解决方案

是的！它被称为 - 它将类别对象映射到类型和态射到术语。因此，键入的lambda（没有名称的函数）或甚至函数可以表示为， Unite类型成为，类型集合（或更复杂的结构）是，并且应用+咖啡因。

I found that there is an isomorphism between logic and programming, called Curry-Howard correspondence, so is there any such equivalence for Category theory, which helps to understand things like Functors or Monads?

解决方案

Yes! It's called Curry–Howard–Lambek - it maps Category objects to types and morphisms to terms. So, typed lambda (function without name) or even function may be represented as cartesian-closed category, where Unite-type becomes a terminal object, set of types (or more complex structure) is product, and apply+currying is exponential.

这篇关于编程中类别的类比是什么？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！