Questions tagged [category-theory]

Category theory is used to formalize mathematics and its concepts as a collection of objects and arrows (also called morphisms). Category theory can be used to formalize concepts of other high-level abstractions such as set theory, ring theory, and group theory. (By Steve Awodey)

Filter by
Sorted by
Tagged with
137 votes
7 answers
40k views

Is Category Theory useful for learning functional programming?

I'm learning Haskell and I'm fascinated by the language. However I have no serious math or CS background. But I am an experienced software programmer. I want to learn category theory so I can become ...
user avatar
31 votes
2 answers
3k views

How are programming languages and foundations of mathematics related?

Basically I am aware of three foundations for math Set theory Type theory Category theory So in what ways are programming languages and foundations of mathematics related? EDIT The original ...
Guy Coder's user avatar
  • 5,091
22 votes
2 answers
1k views

What is meant by Category theory doesn't yet know how to deal with higher-order functions?

In reading Uday Reddy's answer to What is the relation between functors in SML and Category theory? Uday states Category theory doesn't yet know how to deal with higher-order functions. Some day, ...
Guy Coder's user avatar
  • 5,091
19 votes
1 answer
274 views

Natural occurrences of monads that make use of the category-theoretical framework

Today, a talk by Henning Kerstan ("Trace Semantics for Probabilistic Transition Systems") confronted me with category theory for the first time. He has built a theoretical framework for describing ...
Raphael's user avatar
  • 72k
9 votes
3 answers
389 views

Rigorous proof that parametric polymorphism implies naturality using parametricity?

This question asks for an informal explanation of why all polymorphic functions between functors are natural transformations (This is a claim made by Bartosz Milewski). One answer to that question ...
user56834's user avatar
  • 3,632
27 votes
3 answers
4k views

What is the relation between functors in SML and Category theory?

Along the same thinking as this statement by Andrej Bauer in this answer The Haskell community has developed a number of techniques inspired by category theory, of which monads are best known but ...
Guy Coder's user avatar
  • 5,091
17 votes
4 answers
6k views

What exactly is the semantic difference between category and set?

In this question, I asked what the difference is between set and type. These answers have been really clarifying (e.g. @AndrejBauer), so in my thirst for knowledge, I submit to the temptation of ...
user56834's user avatar
  • 3,632
7 votes
1 answer
387 views

How is the definition of monads in category theory equivalent to the definition in functional programming?

In Haskell, Monad is a class of type constructors which act on types that have the following functions implemented: ...
Eben Kadile's user avatar
6 votes
1 answer
236 views

What are some examples of types that can't be derived set theoretically?

I'm hoping for examples that aren't too abstract or useless in day-to-day programming, though not with a lot of hope, since in Bartosz Milewski's book, it is stated that generally speaking, the ...
bbarker's user avatar
  • 163
5 votes
1 answer
870 views

Are there any type constructors which are *not* functors?

So I'm almost done teaching myself category theory. One of the main take-aways for me is that type constructors (higher-kinded types) are endo-functors. But it this always the case? What's throwing ...
gardenhead's user avatar
  • 2,210
4 votes
1 answer
332 views

Why are all polymorphic functions between functors natural transformations?

Bartosz Milewski's Category Theory for Programmers says the following: A parametrically polymorphic function between two functors (including the edge case of the Const functor) is always a natural ...
Max Heiber's user avatar
2 votes
1 answer
235 views

Creating a large tuple from smaller tuples via a monad or applicative

Suppose I have a term $a :\alpha$ of the Simply-Typed Lambda Calculus (in the following, $\alpha, \beta, \gamma$ stand for arbitrary types) and I want to lift it to a term $\lambda x_{\beta}. \;(x, \, ...
user65526's user avatar
  • 194