Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

Via the curry-howard-lambek(-...) correspondence, Category Theory is a pattern language for programming. It has a very rigorous criterion that justifies calling a logical/mathematical/programmatic construct a pattern: a pattern is a universal construction. Bear with me if you would like. I'm doing this off the cuff and I doubt I'm good enough to communicate what I want in a single Internet comment :)

A universal construction, at the vaguest level is the most general way of solving a particular problem. For example: What is the universal way to construct a program that produces two values?

Via curry-howard: A program is an arrow from f : A -> B. We call A and B types, they are like specifications of the environment a program takes and the environment it produces. e.g. (+1) : Int -> Int is the program that takes an Int and produces another Int, by incrementing. We also have a way of composing programs, (.), which to young mathematicians is function composition, to older mathematicians morphism composition, and to nixy programmers the pipe operator (in reverse). (+1) . (x2) : Int -> Int is the program that first multiplies by 2, and then adds 1.

We want a solution that produces two values from the same environment. Such a solution looks like f : W -> A, g : W -> B. That is, we have two programs that take the same environment and each produce their own value.

Let's say our language has product types. That is, given a context A, and a context B, we also have the context A x B. This is a very natural thing to have. A language with pairs/tuples has such a type. What makes product types special is that they come with functions proj_1 : A x B -> A and proj_2 : A x B -> B which do the "obvious thing". That is, the first one just gives you the first element of the pair while the second just gives you the second element of the pair. I claim that this type and its projections are the universal solution to the problem of constructing a program that produces two values.

What do I mean by that? I haven't defined at all what universal means. See, I don't want to give the rigorous definition because it is very abstract and I think it takes a lot of pondering to really understand it. Instead, let me wave my hands some more and give references at the end: A universal construction is something that solves a problem in such a way that any other solution to the problem can be transformed into an instance of this construction.

The functions proj_1 and proj_2 are not the only feature of product types. They have another feature, and it is that, given a solution f : W -> A, g : W -> B, there is a unique way to produce a function W -> A x B, that is, there is a program that converts our solution into a product type. This is usually denoted < f, g > : W -> A x B. Furthermore we have that proj_1 . < f , g > = f and proj_2 . < f , g > = g.

This might either be complete nonsense, a triviality, or something you already understand. This definition of product, when made rigorous and with all its details written in, transfers from programming languages, to logics, to set theory, to algebra, to topology, to geometry and beyond. It is a pattern, and you can use this pattern wherever you find it. And where you don't find it, usually there's significant reasons why it can't exist.

https://en.wikipedia.org/wiki/Universal_property



And nobody cares because it is easier to just use a word Set. Or Program. (in Church-Turing sense, and not awkward Curry-Howard isomorphism)

A true Program is not really an Arrow, as it deals with mutable unknown state that cannot be reduced to a known set of inputs completely. (Where functional and monadic programming gets awkward or impure.) There may also be multiple outputs and inputs at any stage in the process, an Arrow limits you to one output and input vector making actual programming awkward. Forces the kinds of composition you can describe.


yikes.




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: