# Tag Info

### 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
Accepted

You should be more precise. When you say that f(x), f a and m >>= f are "the same", ...
• 31k
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
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
Accepted

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

### 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 ...
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
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
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

### 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
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
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

### 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

### 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

### 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
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
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

### 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

### 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
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
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

### 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

### 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

• 12.1k

### 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
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