# Tag Info

116

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

30

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

29

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

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

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

13

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

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

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 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 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$, ... 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 Asking whether an occurrence of monad is natural is similar to asking whether a group (in the sense of group theory) is natural. Once you formalise something, in this case as an endofunctor, either it satisfies the axioms of being a monad or not. If it does satisfy the axioms, then one gets a lot of technical machinery for free. Moggi's paper Notions of ... 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 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 ...

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