123

In a previous answer in the Theoretical Computer Science site, I said that category theory is the "foundation" for type theory. Here, I would like to say something stronger. Category theory is type theory. Conversely, type theory is category theory. Let me expand on these points. Category theory is type theory In any typed formal language, and even in ...


33

Echoing @AJed advice, I recommend to turn your statement I want to learn category theory so I can become better at Haskell. on its head: learn Haskell, building on your programming intuition. Once you are an FP guru, it might be easier to pick up category theory (if you still care). Category theory is simple for somebody with broad mathematical education ...


31

I'm going to try and keep it short and sweet. There is an informal correspondence between Haskell programs and certain classes of categories, which can be made more formal with some work. This correspondence is known as the Curry-Howard-Lambek correspondence and relates: Haskell types with objects of the category Terms of type $A\rightarrow B$ with ...


29

[Note: this paragraphs is now outdated.] The title of your question contains an unwarranted assumption, namely that programming languages are "based on foundations of mathematics". This is generally not the case, although the two areas do have important relationships. A more accurate statement would be that (some) programming languages were designed using ...


15

The issue with higher-order functions is simple enough to state. A type-constructor like $T(X) = [X \to X]$ is not a functor. It should have been. A polymorphic function like ${\it twice}_X : T(X) \to T(X) = \lambda f.\, f \circ f$ is not a natural transformation. It should have been. If you read Eilenberg and MacLane's original category theory paper,...


15

A Standard ML structure is akin to an algebra. Its signature describes an entire class of algebras of similar shape. A Standard ML functor is a map from a class of algebras to another class of algebras. An analogy is, for instance, with the functors $F : {\bf Mon} \to {\bf Grp}$, which adds an inverse operation to monoids, or $F : {\bf Ab} \to {\bf Rng}$ ...


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

Categories form a (large) category whose objects are the (small) categories and whose morphisms are functors between small categories. In this sense functors in category theory are "higher size morphisms". ML functors are not functors in the categorical sense of the word. But they are "higher size functions" in a type-theoretic sense. Think of concrete ...


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

A short answer: no [but this is only an opinion] Don't go to Category Theory or any other theoretical domain to become good in Haskell. Learn functional programming techniques, such as tail recursion, map, reduce, and others. Read as much code as you can. Implement as many ideas as you can. If you have issues, read and read. If you want a good ...


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


11

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


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.


9

[This second answer presents an outline of what a "Category Theory 2.0", that deals with higher-order functions properly, might look like.] We have known for a long time how to deal with higher-order functions in reasoning about them. When an algebraic structure has higher-order operations, homomorphisms don't work. We must use logical relations instead. ...


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


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

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

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


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

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


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


7

There are at least three encodings of (aspects of) Category Theory in Coq. Approaches using a proof assistant guarantee correctness by design, though I don't know whether they will enhance understand. You'll then have both the proof assistant and Category Theory to learn. If you want a reasonably introductory, computer science-oriented book, it's hard to ...


7

The compiler can optimize exponentiation with monoids. Let $\oplus$ be a binary operator calculateable in constant time such that $\oplus$ and $a_1, a_2, ... \in A$ form a monoid. Then the operation $$\bigoplus_{[1..n]} a_k = \underbrace{a_k \oplus a_k \oplus \dots \oplus a_k}_{\text{$n$ times}}$$ which usually takes $\cal O(n)$ time can be evaluated with ...


7

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


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

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

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


6

this is a very complex topic and there are many great books on the subject, a recent one is called Turings Cathedral, origins of the digital universe and also Engines of logic, mathematicians and the origins of the computer. computer languages have evolved over many decades, but believe it or not there are two original programming languages which show that ...


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


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