3 ms·
CT describes type theory really well, which is used in a lot of programming languages. Monoids and Monads come from CT, and their implementation doesn't really
by proc0 4y ago
CT describes type theory really well, which is used in a lot of programming languages. Monoids and Monads come from CT, and their implementation doesn't really explain what the concept really is (it kind of does, but not really). The programmer might not need to learn CT, but it helps to have broader understanding of how the underlying rules of the language are working.
- School-Cotton 4y agoMonoids do not come from category theory, they come from abstract algebra. How does category theory “describe type theory” ?
- trenchgun 4y agoIt can give semantics for it, such as how cartesian closed category gives semantics to simply typed lambda calculus https://golem.ph.utexas.edu/category/2006/08/cartesian_closed_categories_an_1.html https://golem.ph.utexas.edu/category/2006/08/cartesian_close...
- deterministic 4y agoNope. Type Theory (like Matin Luff TT) describes Type Theory really well. And it is way more useful for software development than CT is. Tools like Coq, LEAN, Agda, Idris etc. are built on TT not CT.