19
votes
What exactly is the semantic difference between category and set?
In brief, set theory is about membership while category theory is about structure-preserving transformations – but only about the relationships between those transformations.
Set theory is only about ...
- 390
16
votes
Accepted
“Left identity” of Monad laws in Haskell is wrong
You should be more precise. When you say that f(x), f a and m >>= f are "the same", ...
- 31k
15
votes
Accepted
Reference request: Category theory as it applies to type systems
Category theory is not necessary to understand programming languages, it's not even necessary to do advanced research on programming languages. Most programming language people don't know (much) ...
- 8,358
15
votes
Accepted
Is there an isomorphism between (subset of) category theory and relational algebra?
Let me articulate the Curry-Howard-Lambek correspondence with a bit of jargon which I'll explain. Lambek showed that the simply typed lambda calculus with products was the internal language of a ...
- 12.1k
15
votes
Accepted
Monad in Haskell programming vs. Monad in category theory
A monad in Haskell is intended to be a monad on the category of types, when the category theory is done internally to the type theory. The capabilities of Haskell and similar languages are somewhat ...
- 2,792
13
votes
Rigorous proof that parametric polymorphism implies naturality using parametricity?
The missing part is the "identity extension lemma", which is mentioned in Reynolds' original paper but not in Wadler's.
For $F : \text{Type} \to \text{Type}$, this says that if the ...
- 948
11
votes
Accepted
What are some examples of types that can't be derived set theoretically?
There are several type-theoretic constructions that cannot be easily handled with set theory. Note that when we say "set theory" we mean that we intend to interpret types as sets and type-theoretic ...
- 31k
11
votes
Accepted
Are there any type constructors which are *not* functors?
One obvious counterexample is a binary search tree. You cannot freely substitute the values in a binary search tree because a substitution might change the ordering (relative to ...
- 23.1k
10
votes
Accepted
A monad is just a monoid in the category of endofunctors, what's the enlightenment?
This answer may not be exactly what you are looking for. That is, I think perhaps the importance of this characterisation is being overemphasised here. The quote
a monad in X is just a monoid in the ...
- 661
10
votes
What exactly is the relation between Haskell and category theory?
Category theory is an abstract branch of mathematics and you do not need to learn it before you start writing Haskell code. Similarly, you do not need to learn Haskell before you start learning ...
- 296
9
votes
Accepted
How is the definition of monads in category theory equivalent to the definition in functional programming?
The Haskell monads are known as Kleisli triples in mathematics. I am guessing you're coming from the Haskell land, so let me just put down the translations between the two formulations in Haskell (I ...
- 31k
9
votes
Accepted
Can the formalisms of category theory replace those of type theory?
Since you say that "the subtleties of the correspondence between type theory and category theory are outside your ken", perhaps the best way to understand the correspondence is to read non-technical ...
- 31k
9
votes
Can the formalisms of category theory replace those of type theory?
My view is more or less similar to chi's. I see category theory as (roughly) being to type theory what model theory is to logic. Some of the consequences of that are, first, each can exist ...
- 12.1k
9
votes
Why are the laws of an applicative functor defined the way they are?
As described in the original idioms paper, Applicative (called Idiom there) corresponds to a strong lax monoidal functor. This ...
- 12.1k
7
votes
Semantic readings of the Lambek sequent calculus
What constitutes a proof in a system like this is a derivation which is a tree of rule applications. The above translation function is defined by (structural) recursion over that tree. Note, this is ...
- 12.1k
7
votes
Accepted
Generators in category theory
The most obvious intuition comes from the notion of well pointed categories. A well pointed category is simply a category $\cal C$ in which the final object $1$ exists and is a generator for $\cal C$. ...
- 8,262
7
votes
Accepted
Given A to C, and B to C with known complexities, what can be said about A to B?
We can have sets $A, B, C$ with linear-time computable maps $f : A \to C$ and $g : B \to C$ such that there exists a map $h : A \to B$ with $f = g \circ h$, but the needed time complexity/Turing ...
- 3,213
7
votes
Functional Programming and Category Theory
These colleagues of yours, would they happen to be Haskell aficionados?
They might have told you that Hask was a category made from Haskell, but that is a lie, notheless a very useful one that ...
- 31k
7
votes
Set theory pertaining to category theory and functional programming
The notation $f:E\times F \to G$ means that $f$ is a function that needs two arguments, one from $E$, one from $F$, and the image is in $G$.
This is how the function $\text{Union}$ is defined: the two ...
- 16k
6
votes
Accepted
Writing the coherence conditions for a monad in a functional laguage
First off, you've confused $\nu$ and $\eta$ in your class. I'm going to go with $\eta$.
The coherency law:
$$\mu \circ T \eta = \mu \circ \eta T = 1_T$$
translates to:
...
- 23.1k
6
votes
Accepted
Can we define a program by means of a walk of a graph induced by the category of types?
Consider the simply-typed $\lambda$ calculus: this is one of the simplest functional languages you can define.
It is very common to interpret it in a Cartesian closed category (CCC). Indeed, CCCs are ...
- 14.6k
6
votes
Reference request: Category theory as it applies to type systems
Learning category theory is a huge time investment, and the question whether it is worth it is very valid. I still struggle with this too, and I already know why I should learn it. I wrote:
I liked ...
- 5,400
5
votes
functional programming in terms of Set
You can use the category of sets as your model of how functional programming works as long as you do not allow general recursive definitions.
To see why general recursion is not valid in the category ...
- 31k
5
votes
Can we define a program by means of a walk of a graph induced by the category of types?
Your question sounds redundant to me. By definition of category whenever two morphisms with common object $f\colon A \rightarrow B$ and $g\colon B \rightarrow C$ exist, then their composition $g\circ ...
- 1,205
5
votes
What exactly is the semantic difference between category and set?
Category theory is in some sense a generalization of set theory: the category $C$ could be the category of sets, or it could be something else. So, you learn less if you learn that $x$ is an object ...
D.W.♦
- 164k
4
votes
What exactly is the semantic difference between category and set?
A further point on D.W.'s explanation
There's no difference between saying that $x$ is a group vs saying that $x$ is an object in the category $\mathsf{Grp}$. Those two statements are equivalent.
...
- 1,205
4
votes
Accepted
How to explain/understand brackets of applicative functor [[f u1... un]]?
In it's simplest, original form, $[\![f\ x \ y]\!]$ just means $\eta(f)\circledast x \circledast y$ where $\circledast$ is what Haskell calls <*> and $\eta$ ...
- 12.1k
4
votes
functional programming in terms of Set
A typical mindset would be to consider them separate categories:
Category of types and programming functions
Category of sets and set
functions
We can then ask questions such as:
Is there functors ...
- 1,205
4
votes
Accepted
What is a not-well-founded cotree?
I'm not sure what you mean by "all relations are inverted" (what's the relation of a tree?), but perhaps I can provide some insight.
In Haskell, one might write the type of binary trees as such:
<...
- 8,262
4
votes
Accepted
How to determine whether a dependent type that doesn't fit the monad instance is categorically a monad
So, there are potentially many answers to this sort of question. One is that there are many possible categories on which there can be monads. The rules for establishing that something is a monad will ...
- 2,792
Only top scored, non community-wiki answers of a minimum length are eligible