15

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) category theory. Category theoretical methods have been useful mostly in a small part of programming language research, namely in the analysis of functional ...


14

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 cartesian closed category. I'm not going to spell out what a cartesian closed category is, though it isn't difficult, instead what the above statement says is you ...


14

You should be more precise. When you say that f(x), f a and m >>= f are "the same", that does not make sense as written. f(x) and f a cannot be the same, they do not even use the same variables. Did you mean to compare f(u), f u and u >>= f? It is true that f(u) and f u are the same thing, but u >>= f is not. If f has type a -> m b (...


13

Well, that of course depends on what sort of program you are trying to design. If you are designing an accounting program for your aunt's chocolate shop, I very much doubt category theory will be of much use. But there are of course situations in which category theory is enormously useful in design of programs (by which I also mean data structures, ...


13

In brief, set theory is about membership while category theory is about structure-preserving transformations. Set theory is only about membership (i.e. being an element) and what can be expressed in terms of that (e.g. being a subset). It does not concern itself with any other properties of elements or sets. Category theory is a way to talk about how ...


12

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 limited, so there are a lot of basic constructions in category theory that cannot be done, but there are plenty of structures that can be encoded reasonably. M ::...


10

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 types, only the coinductive ones. Many people are in denial about this particular issue.


10

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 functions as set-theoretic functions. In particular, the set-theoretic interpretation of types requires that a function type A → B must be interpreted as the set ...


9

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 Ord), or even replace the values with a type which is not an instance of Ord at all. A possibly less-obvious example is a contravariant endofunctor. Consider: data Tricky a = ...


9

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 expositions on the topic. I can recommend two: Steve Awodey, From Sets to Types, to Categories, to Sets, In: Sommaruga G. (eds) Foundational Theories of ...


9

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 autonomously. Indeed, type theory predates category theory, and the creation of category theory was not motivated by these concerns. Second, many of the distinctions ...


9

As described in the original idioms paper, Applicative (called Idiom there) corresponds to a strong lax monoidal functor. This can be formulated as: class (Functor f) => MFunctor f where unit :: () -> f () pair :: (f a, f b) -> f (a, b) The applicative functor laws are then equivalent to the above operations being "monoidal" in the ...


8

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 functor $F$ in this case is $$F(X)=X\times X+X+1.$$ Think of this as representing the three different operators. The first component of the sum, $X\times X$, ...


8

Your intuition is correct: terms are "somehow" elements of the objects. The only thing left is to figure out what elements in a category are. They cannot be literally elements because objects need not be sets (and more generally there may be no way to even "convert" an object to a set with a functor). If I say "consider a mass point $p$ moving in $\mathbb{R}...


8

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 define everything from scratch on purpose and avoid clashes with standard notation): {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE FlexibleInstances #-} ...


8

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 category of endofunctors of X is originally from Mac Lane's Categories for the Working Mathematician, where it appears as a helpful intuition for the ...


7

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 why it labels the premises in the rules with $\delta$. This is intended to be mnemonic for "derivation". I'm guessing but $\mu$ and $\nu$ appear to need to be ...


7

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$. This means that for every $f,g:A \rightarrow B$, $$ f = g \ \Leftrightarrow \forall p:1\rightarrow A, f\circ p = g\circ p$$ Note that $\circ$ is composition ...


7

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 degree for $h$ is as high as you want. Proof: Pick a map $H : \Sigma^* \to \Sigma^*$ which is hard in whatever sense you have chosen. Now let $A = C = \Sigma^*$, ...


7

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 arguments $A$, $B$ are in $\mathcal{P}(X)$ and the image $\text{Union}(A, B) = A\cup B$ is in $\mathcal{P}(X)$.


6

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 assembly language when I started to program, and set theory feels similar to assembly language. Category theory is one alternative to get around all the ...


6

People used to use CT to describe data types. The data type was defined by a particular category whose objects are finite sequences of (specification language) types, and whose arrows were projections or else compositions of the data type operations. For example, the object is the domain and is the codomain of the push operation of stacks. This ...


6

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 Goguen used a category of automata as an example in his Categorical Manifesto. (He also did research on such categories.) That such categories exist makes no ...


6

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: mu . fun eta = mu . eta = id And the other coherency law: $$\mu \circ T\mu = \mu \circ \mu T$$ translates to: mu . fmap mu = mu . mu Intuitively, the reason why the $T$ "disappears" ...


6

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 the "ideal" categorical setting where to interpret simple types. CCCs, being categories, admit morphisms composition and identity. Taking your definition of "...


6

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 relational interpretation of $F$ is instantiated with a type $A$ and the identity relation on $A$, we get the identity relation on $F\,A$. For System F, identity ...


5

The proper thing is to setup data ListF a x = Nil | Cons a x Now you can write newtype Mu f= Mu (forall a.(f a->a)->a) data Nu f = forall a. Nu a (a->f a) In Haskell we can observe that Mu ListF and Nu ListF coincide. So, it can be either (!). (one source on this claim: http://www.cs.ox.ac.uk/jeremy.gibbons/publications/adt.pdf) Additionally, ...


5

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 something that directly corresponds to the simply typed lambda calculus without implying products check out this paper by Bart Jacobs: Simply Typed and Untyped Lambda Calculus Revisited. Let's ...


5

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 of sets, consider the following program (written in Haskell): fix :: (Bool -> Bool) -> Bool fix f = f (fix f) If we interpret Bool as any set $B$ with ...


5

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 f \colon A \rightarrow C$ must exists as another arrow in that same category. (otherwise, that situation is just not a category.) So the redundant part in your ...


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