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) ...
user avatar
15 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 ...
user avatar
  • 304
14 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 ...
user avatar
14 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", ...
user avatar
14 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 ...
user avatar
  • 2,005
10 votes

Which fixpoint is Haskell list type?

It's the greatest fixed point, or the final coalgebra, depending on how you set things up. In Haskell it is impossible to define the datatype of finite lists because Haskell does not have inductive ...
user avatar
10 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 ...
user avatar
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 ...
user avatar
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 ...
user avatar
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 ...
user avatar
9 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 ...
user avatar
  • 18.7k
9 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 ...
user avatar
  • 556
8 votes
Accepted

Intuition behind F-algebra

Given a functor $F:Set\to Set$, an $F$-algebra is just a function $f:F(X)\to X$, where $X$ is some set known as the carrier set. In your example, $X$ is the set of elements of some group. The endo ...
user avatar
8 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 ...
user avatar
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 ...
user avatar
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$. ...
user avatar
  • 7,734
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 ...
user avatar
  • 1,904
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 ...
user avatar
  • 6,932
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 ...
user avatar
6 votes

DFAs as Categories

As David Richerby stated, you can make a category out of just about anything, so of course automata in their various forms are included. Googling "category of automata" will return results and Joseph ...
user avatar
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: ...
user avatar
  • 18.7k
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 ...
user avatar
  • 14.1k
6 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 ...
user avatar
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 ...
user avatar
5 votes

How precise is the statement "STLC is the internal language of CCCs"?

Cartesian closed categories correspond to the simply typed lambda calculus with products. Your silly function is just $\lambda x.\lambda y.y$. If you want ...
user avatar
5 votes
Accepted

Which fixpoint is Haskell list type?

The proper thing is to setup data ListF a x = Nil | Cons a x Now you can write ...
user avatar
  • 266
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 ...
user avatar
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 ...
user avatar
  • 140k
5 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 ...
user avatar
4 votes
Accepted

Definition of opposite category

The problem in your first example is that the arrows don't compose. In the first, you have $f: A \leftarrow B$ and $g: C \leftarrow B$, so $f\circ g$ is not in $C$, hence in $C^{op}$ $f : B \leftarrow ...
user avatar

Only top scored, non community-wiki answers of a minimum length are eligible