# Tag Info

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

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

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

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

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

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

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

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

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

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

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

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

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