functional programming in terms of Set

I'm writing some notes about functional programming, so I'd want to describe some features of the category theory.

I visited wiki page about Category of Set, and I found this:

"The epimorphisms in Set are the surjective maps, the monomorphisms are the injective maps, and the isomorphisms are the bijective maps".

I'd want to explain Category theory it in term of computer science, so my question is:

• It's correct to consider only the category of Set?
• It's correct to consider only the category of Set when I explain functional programming in term of Monoid/Functor/Algebraic Data/Product type and so
on?

I know that Category theory is not only Set, but It's important for me define a boundary where all my examples are correct on assumptions and definitions.

thanks Mike.

migrated from stackoverflow.comMay 16 '17 at 19:38

This question came from our site for professional and enthusiast programmers.

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 at least two elements (for instance $B = \{0, 1, \bot\}$) then there will be a map $f : B \to B$ which does not have a fixed point (for instance $f(0) = 1$, $f(1) = \bot$, $f(\bot) = 0$). However, fix always computes fixed points.

You can use sets as long as all the recursive definitions are well-founded, i.e., the recursive calls always happen on strictly smaller arguments. Typical fold and map operations on lists and other inductively defined structures are like that.

To model recursion one has to change something. One possibility is to use domains which were invented precisely for this purpose.

A typical mindset would be to consider them separate categories:

1. Category of types and programming functions
2. Category of sets and set functions

We can then ask questions such as:

• Is there functors between them?
• Do they both have product, coproduct, endofunctors...?
• Can they be made Cartesian closed categories?

Why separate them? It is more flexible. Depending on your idea of functional programming or specific programming language, sooner or later, you might spot the differences. For a mundane example, maybe the initial object and terminal object in your programming language is the one and only null type, but you know that this is not the case the the category $Set$.

On the other hand, $Set$ is a perfectly fine place to do programming inside. You can define what is Boolean, natural number, conditional statements ... inside $Set$. (Actually, except for general recursion. See Andrej Bauer's answer for this)

• Wouldn't the initial object and terminal object be the empty and unit types, respectively? – gardenhead May 17 '17 at 0:21
• Point is, it depends on the language, right? – Apiwat Chantawibul May 17 '17 at 6:32

Generally, programming languages only make use of a single category - the category of all available types. If the type system is sufficiently simple, we may take that category to be Set; but usually it is just some arbitrary category of types. We can still talk about Monoids/Functors/Natural Transformations etc, but use just a single category in those definitions. For example, all functors in programming (type constructors) are endofunctors.

N.B. I am not an expert in category theory

I'd want to explain Category theory it in term of computer science, so my question is:

• It's correct to consider only the category of Set?
• It's correct to consider only the category of Set when I explain functional programming in term of Monoid/Functor/Algebraic Data/Product type and so on?

I believe you mixed up 2 questions.

1. How to explain category theory in terms of computer science?
2. How to explain computer science in terms of category theory?

Question 2 was addressed in other answers, so I will focus on Question 1.

Suppose you consider only the category of sets and functions when teaching category theory. I would not say that this method is incorrect because "correctness" does not make sense in this context to me. I would say that it is useless. As an abstract branch of mathematics, category theory consists of theories (examples: category, monoidal category, category with finite products) and models of those theories (examples: the category of sets, categories of algebraic structures, categories of domains). Any theorem deduced from a theory is true for every model of that theory. Cost–benefit analysis of this approach follows.

• Benefit. The approach saves thought, so to speak. If we know $n$ models of a theory, every proof yields $n$ theorems instead of $1$.
• Cost. Theories lie on the next level of abstraction. Abstraction is hard.

The more models, the more useful is the theory. No need to dive into category theory if you wish to reap the benefits of abstraction. Abstract algebra, order theory, topology, and other branches were built on the same principle.

After this long prelude, I hope it is clear why I called it useless. If you consider only the category of sets, $n=1$. The benefit is 0, but the cost still exists. The whole point of abstraction is lost. If you do not need the benefits of abstraction, why stress yourself with abstraction? In this case, why explain or learn category theory in the first place?

Thanks for all answers. What I thought is that category of Set was 'similar' (Arrgh! when I speak with mathematicians every word may be not correct) than the others. In programming languages, objects are types and morphisms are functions so I thougtht that the category of Set was ok, except for general recursion. Now I understand that the right way is the category of all available types. I like to know how define mono and epic morphisim in terms of category of all available types. It's clear for me the means in the category of Set, because the injectivity and surjectivity are strictly related to the monomorphism and epimorphism, but not in category of all available types. Probably I have to study!

Now, what I want to describe in my document is a little bit of theory or abstraction if you prefer, related to a functiona programming objects. Example:

Each type A in Hask is transformed to TC[A]. List[Int] is a type constructor then a functor is F: Int → List[Int]

So to explain about Functor (endofunctor) and what 'preserve the stucture' is meaning, the category theory comes in handy.

The same for Product/Coproduct when I want to explain Algebraic Data Type.

Mike.

• Take monomorphism for example. Lots of programming languages are built with $Set$ perspective --- that type are things inhibited by some value and functions are just value mapping, so it's tempting to conclude monomorphism is just injective map. But for me, I like to retain a more open minded because I'm concerned by function being concurrent and/or have side-effects. So I personally thought of monomorphism as process which "retains the identity of $x$ when post-compose to $x$". – Apiwat Chantawibul May 19 '17 at 14:13
• I don't know a good term for it, but the closest comparison I find is to reversible process. Note the difference between invertible morphism and monomorphism. For left-invertible process (I like to call it post-invertible process), not only you know the identity of whatever $x$ it post-composes to, you can also get the $x$ back by post-composing again with the inverse. However, for monic process, you can deduce the identity of $x$ but not get it back by any further processing. – Apiwat Chantawibul May 19 '17 at 14:22
• BTW, you're probably using the site wrong. This looks more like an additional clarification to original answer than an actual answer... Well, but I'm no moderator. – Apiwat Chantawibul May 19 '17 at 14:35
• $Set$ is an important example, but it is a common mistake to pretend all categories are similar to $Set$. Even in programming languages, we know that $Set$ is not good enough to model polymorphic types (look up Reynold's "polymorphism is not set-theoretic"), hence if we want models for polymorphism we need more complex categories than $Set$ (e.g. PERs). Keep $Set$ in mind as a familar case, but don't expect everything acts always like in $Set$. (You might also want to look up "concrete categories") – chi May 19 '17 at 19:22