Here I am in Cadiz to attend 2017 edition of Lambda World. Cadiz is really a nice frame for this conference and the weather is so good that it seems to be back at vacation time instead then in mid-Autumn.
Anyway, on this morning I attended the “unconference”, a sort of informal prelude to the real conference. After the first, planned talk, people could register to present their talk and other attendants could vote their preferred talk. This yield two interesting talk – one on declarative testing and the other one on category theory. Here is what I learned from the last one, by Rùnar Bjarnason.
First, this is algebra stuff, really. Not the kind of ‘a+b’ you do in mid schools, but the high order stuff you do later when you study groups, monoids and the likes.
How does these concepts applies to practical programming still eludes me, but I sense that something is there waiting for my brain to grasp it.
Basically an abstract algebra of function wants to answer to the following questions – what functions do? And what can we say about them? Here we go, all mistakes, errors, inconsistencies are just mine, blame me not Rùnar.
A Category is defined by objects and arrows and how we can compose those arrows.
If you consider language types as objects then functions can be thought as arrows from an object to another object:
Some types: A, B, C.
Some functions f, g.
f: A => B g: B => C
a composite functions is formed by invoking a function on the result of another one:
g compose f = (x => g(f(x)))
As long as types line up we can concatenate function composition.
If a function links an object to itself (in the example a type to itself), this is the identity function:
identity function: identity[A] : A=>A identity compose f = f f compose identity = f
Sometime composition is expressed with a dot. An interesting property is that composition is associative:
h.g.f = (h.g).f = h.(g.f)
(so no need for parenthesis).
In Scala you have a category for functions and types, but also for types and inheritance (subtyping). This category is defined as follows:
Objects: Scala Types: A, B, C…
Arrows: Subtype relations: A <: B, B <: C…
Composition: [ A <: B, B <: C ] => A <: C
Associativity: A <: B <: C (no need for parenthesis)
Identity: A <: A
Another example of category is the the pre-order (<=). Objects are instances of a Type on which <= binary relationship is defined:
Objects a, b, c…
Arrows: a <= b, b <= c
Transitivity: <=
Identity: a <= a
E.g. natural numbers are a category for preorder.
Monoids are categories with one object. This object, by convention, is written as ‘*’. All arrows links * to itself. In a turn of notation I’ll use the symbol |+| for composition and ‘mzero’ for identity.
Objects: *
Arrows: f, g, h: * -> *
associativity
identity: * -> *
mzero |+| a = a
a |+| mzero = a
Object is just an anchor, to hold arrows.
Category of preorders:
A preorder is a set with <=
Objects: all the preorders (Scala integers)
arrows: Homomorphisms on preorders
[NdM: at this point things start to be complicated and I have likely lost the speaker. What follows are likely to be glimpses of his talk… the parts I got]
Monotonic functions.
e.g. string length : _.length is a monotonic function.
Preserves relationship:
x <= y then h(x) <= h(y)
Category of monoids:
Objects: all the monoids
Arrows: monoid homomorphism
h( x |+| y) == h(x) |+| h(y)
Category of categories
Objects: all the categories
Arrows: category homomorphism F
F( f . g ) = F(f) . F(g) e.g. _map( f compose g ) = _.map(f) compose _.map(g)
these are functors.
Given a category C, there is a category of endofunctors on C
endofunctor F[_]
Objects: functors
arrows: functor homomorphism
h: F[A] => G[A]
h compose _.map(f) = _.map(f) compose h
trait ~>[F[_].G[_]] { def apply[A](a: F[A]) : G[A] }
A monad on C is an endofunctor M[_] together with two natural transformations:
pure[A] : A=>M[A]
join[A] : M[M[A]] => M[A]
A monad is a kind of category:
M[M[M[A]]] : can be associated as we want, preserving the result.
A monad is a monoid in an endofunctor category.
[And with this truth the brief talk is over]