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) ...
• 8,168

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 ...
• 304
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 ...
• 11.8k
Accepted

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

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 ...
• 28k
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 ...
• 28k
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 ...
• 28k

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 ...
• 11.8k

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 ...
• 11.8k
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 ...
• 18.7k
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 ...
• 556
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 ...
• 20k
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 ...
• 28k

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 ...
• 11.8k
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$. ...
• 7,734
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 ...
• 1,904

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 ...
• 6,932

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,312

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 ...
• 11.8k
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: ...
• 18.7k
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.1k

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 ...
• 28k

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 ...
• 11.8k
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 ...
• 266