{"id":3641,"date":"2019-06-07T12:14:34","date_gmt":"2019-06-07T16:14:34","guid":{"rendered":"http:\/\/www.goodmath.org\/blog\/?p=3641"},"modified":"2019-06-07T12:15:15","modified_gmt":"2019-06-07T16:15:15","slug":"3641","status":"publish","type":"post","link":"http:\/\/www.goodmath.org\/blog\/2019\/06\/07\/3641\/","title":{"rendered":"Category Theory Lesson 3: From Arrows to Lambda"},"content":{"rendered":"

Quick personal aside: I haven’t been posting a lot on here lately. I keep wanting to get back to it; but each time I post anything, I’m met by a flurry of crap: general threats, lawsuit threats, attempts to steal various of my accounts, spam to my contacts on linkedin, subscriptions to ashley madison or gay porn sites, etc. It’s pretty demotivating. I shouldn’t let the jerks drive me away from my hobby of writing for this blog!<\/em><\/p>\n

I started this series of posts by saying that Category Theory was an extremely abstract field of mathematics which was really useful in programming languages and in particular in programming language type systems. We\u2019re finally at one of the first places where you can really see how that\u2019s going to work.<\/p>\n

If you program in Scala, you might have encountered curried functions. A curried function is something that\u2019s in-between a one-parameter function and a two parameter function. For a trivial example, we could write a function that adds two integers in its usual form:<\/p>\n

  def addInt(x: Int, y: Int): Int = x + y\n<\/pre>\n
That\u2019s just a normal two parameter function. Its curried form is slightly different. It\u2019s written:<\/p>\n
  def curriedAddInt(x: Int)(y: Int): Int = x +y\n<\/pre>\n
The curried version isn\u2019t actually a two parameter function. It\u2019s a shorthand for:<\/p>\n
  def realCurrentAddInt(x: Int): (Int => Int) = (y: Int) => x + y\n<\/pre>\n
That is: currentAddInt<\/code> is a function which takes an integer, x, and returns a function which takes one parameter, and adds x to that parameter.<\/p>\n
Currying is the operation of taking a two parameter function, and turning it into a one-parameter function that returns another one-parameter function – that is, the general form of converting addInt<\/code> to realAddInt<\/code>. It might be easier to read its type: realCurrentAddInt: Int => (Int => Int)<\/code>: It\u2019s a function that takes an int, and returns a new function from int to int.<\/p>\n
So what does that have to do with category theory?<\/p>\n
One of the ways that category theory applies to programming languages is that types and type theory turn out to be natural categories. Almost any programming language type system is a category. For example, the figure below shows a simple view of a programming language with the types Int<\/code>, Bool<\/code>, and Unit<\/code>. Unit<\/code> is the initial object, and so all of the primitive constants are defined with arrows from Unit<\/code>.<\/p>\n
\"\"<\/a><\/p>\n
For the most part, that seems pretty simple: a type T <\/code>is an object in the programming language category; a function implemented in the language that takes a parameter of type A<\/code> and returns a value of type B\u00a0<\/code>is an arrow from A<\/code> to B<\/code>. A multi-parameter function just uses the cartesian product: a function that takes (A, B)<\/code> and returns a C<\/code> is an arrow from A \\times B \\rightarrow C.<\/p>\n
But how could we write the type of a function like our curried adder? It\u2019s a function from a value to a function. The types in our language are objects in the category. So where\u2019s the object that represents functions from A<\/code> to B<\/code>?<\/p>\n
As we do often, we\u2019ll start by thinking about some basic concepts from set theory, and then generalize them into categories and arrows. In set theory, we can define the set of functions from A to B as: B^A={f: A \\rightarrow B} – that is, as exponentiation of the range of the produced functions.<\/p>\n