Why Kleisli Arrows Matter

We're going to take a departure from the style of articles regularly written about the Kleisli category, because, firstly, there aren't articles regularly written about the Kleisli category.

That's a loss for the world. Why? I find the Kleisli category so useful that I'm normally programming in the category, and, conversely, I find most code in industry, unaware of this category, is doing a lot of the work of (unintentionally) setting up this category, only to tear it down before using it effectively.

So. What is the Kleisli Category? Before we can properly talk about this category, and its applications, we need to talk about monads. 

Monads

A monad, as you can see by following the above link, is a domain with some specific, useful properties. If we have a monad, T, we know it comes with an unit function, η, and a join function, μ. What do these 'thingies' do?

• T, the monadic domain, says that if you are the domain, then that's where you stay: T: T → T.

"So what?" you ask. The beauty of this is that once you've proved you're in a domain, then all computations from that point are guaranteed to be in that domain.

So, for example, if you have a monadic domain called Maybe, then you know that values in this domain are Just some defined value or Nothing. What about null? There is no null in the Maybe-domain, so you never have to prove your value is (or isn't) null, once you're in that monadic domain.

• But how do you prove you're in that domain? η lifts an unit value (or a 'plain old' value) from the ('plain old') domain into the monadic domain. You've just proved you're in the monadic domain, simply by applying η.

η null → fails

η some value → some value in T.

• We're going to talk about the join-function, μ, after we define the Kleisli category.

The Kleisli Category

Okay. Monads. Great. So what does have to do with the Kleisli category? There's a problem with the above description of Monads that I didn't address. You can take any function, say:

f : A → B

and lift that into the monadic domain:

f^T : T A → T B

... but what is f^T? f^T looks exactly like f, when you apply elimination of the monadic domain, T. How can we prove or 'know' that anywhere in our computation we indeed end up in the monadic domain, so that the next step in the computation we know we are in that monadic domain, and we don't have to go all the way back to the beginning of the proof to verify this, every time?

Simple: that's what the Kleisli category does for us.

What does the Kleisli category do for us? Kleisli defines the Kleisli arrow thusly:

f^K : A → T B

That is to say, no matter where we start from in our (possibly interim) computation, we end our computation in the monadic domain. This is fantastic! Because now we no longer need to search back any farther than this function to see (that is: to prove) that we are in the monadic domain, and, with that guarantee, we can proceed in the safety of that domain, not having to frontload any nor every computation that follows with preconditions that would be required outside that monadic domain.

null-check simply vanishes in monadic domains that do not allow that (non-)value.

Incidentally, here's an oxymoron: 'NullPointerException' in a language that doesn't have pointers.

Here's another oxymoron: 'null value,' when 'null' means there is no value (of that specified type, or, any type, for that matter). null breaks type-safety, but I get ahead of myself.

Back on point.

So, okay: great. We, using the Kleisli arrows, know at every point in that computation that we are in the monadic domain, T, and can chain computations safely in that domain.

But, wait. There's a glaring issue here. Sure, f^K gets us into the monadic domain, but let's chain the computation. Let's say we have:

g^K : B → T C

... and we wish to chain, or, functionally: compose f^K and g^K? We get this:

g^K ∘ f^K ⇒ A → T B → TT C

Whoops! We're no longer in the monadic domain T, but at the end of the chained-computation, we're in the monadic domain TT, and what, even, is that? I'm not going to answer that question, because 1) who cares? because 2) where we really want to be is in the domain T, so the real question is: how do we get rid of that extra T in the monadic domain TT and get back into the less-cumbersome monadic domain we understand, T?

• That's where the join-function, μ, comes in.

μ : TT A → T A

The join-function, μ, of a monad, T, states that when you join a monad of type T to a monad of that same type, the result, TT, when joined, simplifies to that (original) monad, T.

It's as simple as that.

But, then, it's even simpler than that, as the Kleisli arrow anticipates that you're starting in a monadic domain and wish to end up in that domain, so the Kleisli arrow entails the join function, μ, 'automagically.' With that understanding, we rewrite standard functional composition to composition under the Kleisli category:

g^K ∘^K f^K ⇒ A → T B → T C

Which means we can now compose as many Kleisli arrows as we like, and anywhere we are in that compositional-chain, we know we are in our good ole' safe, guaranteed monadic domain.

Practical Application

We've heard of the Maybe monad, which entails semi-determinism, this monad is now part of the core Java language as the Optional-type, with practical application in functional mapping, filtering and finding, as well as interactions with data-stores (e.g.: databases).

Boy, I wish I had that back in the 1990's, developing the Sales Comparison Approach ingest process of mortgage appraisal forms for Fannie Mae. I didn't. I had Java 1.1. A glaring 'problem' we had to address with ingesting mortgage appraisals what that every single field is optional, and, as (sub-)sections depend on prior fields, entire subsections of the mortgage appraisal form were dependently-optional. The solution the engineering team at that time took was to store every field of every row of the 2000 fields of the mortgage appraisal form.

Fannie Mae deals with millions of mortgage appraisals

Each.

Year.

Having rows upon rows (upon rows upon rows) of data tables of null values quickly overloaded database management systems (at that time, and, I would argue, is tremendously wasteful, even today).

My solution was this, as each field is optional, I lifted that value into the monadic domain, that way, when a value was present, follow-on computations, for follow-on (sub-)sections would execute, and, as the process of lifting failed on a null-value, follow-on computations were automagically skipped for absent values. Only values present were stored. Only computations on present values were performed. The Sales Comparison Approach had over 600 fields, all of them optional, many of them dependently-optional, and only the values present in those 600 fields were stored. The savings in data storage was exponentially more efficient for the Sales Comparison Approach section as compared to the storage for the rest of the mortgage appraisal.

Although easy enough, and intuitive, to say, actually implementing Kleisli Arrows in Java 1.1 (the langua fraca for that project) required I first implement the concept of both Function and Functor, using inner classes, then I needed to implement the concept of Monad, then Maybe, then, with monad, I needed to implement the Kleisli Arrow monadic-bind function to be able to stitch together dozens and hundreds of computations together, without one single explicit null-check.

The data told me if they were present, or not, and, once lifted into the monadic domain, the Kleisli arrows stitched together the entire Sales Comparison Approach section, all 600 computations, into a seamless and concise workflow.

Summary

Kleisli arrows: so useful they are recognized as integral to the modern programming paradigm. What's fascinating about these constructs is that they are grounded in provable mathematical forms, from η to μ to Kleisli-composition. This article summarized the mathematics underpinning the Kleisli category and showed a practical application of this pure mathematical form that translated directly into space-efficient and computationally-concise software delivered into production that is still used to this day.

oh : so True

So, ...

So, I'm going to say 'so' a lot in this post. You'll find out why this is, soonest.

soon, adv: composite word of the words 'so' and 'on.'

Amirite? Or amirite!

SO!

Today's 1HaskellADay challenge wasn't really a challenge, per se, so much as it was an observation, and that observation, keen as it might be...

keen, adj.: composite word of 'ki' (棋) and 'in' (院), transliteration from the Japanese: School of weiqi.

... was that the mapping function from one domain to a co-domain, and the corresponding co-mapping function from the co-domain to the domain gives you, when composed, the identity function in the domain or co-domain.

No, really! That was today's challenge.

To translate that into English:

f : a -> b
g : b -> a

(f . g) : a -> a
(g . f) : b -> b

Wowsers!

So, we're not going to dwell on this, as Eilenberg and Mac Lane have dwelt on this so much better than I, but ...

Okay, so how do we prove this for our

CatA (being Either a a) and
CatB (being (Bool, a))?

With Haskell, it's easy enough, run your functions through quickcheck and you've got a PGP, that is: a pretty good (kinda) proof of what you want.

Or, you could actually prove the thing.

'You' meaning 'I,' in this particular case, and, while proving the thing, actually learn some me some more Idris for greater good.

Let's do that.

So, my last post have looked at a bit of proof-carrying code, and my methodology was to create a predicate that said whether some supposition I had held (returning a Bool, and, I hoped, True, at that!), unifying that with True, and then using the reflexive property of equality to prove that my supposition held.

Well, super neat, but today's problem was much harder for me, because I wrote something like this for one of my proofs:

leftIsomorphism : Eq a => (Bool, a) -> Bool
leftIsomorphism pair = (f . g) pair == pair

That, as far as it goes is just what we want, but when we try to prove it with this function:

isEqLeftTrue : Ea a => (val : a)
-> leftIsomorphism (True, val) = True
isEqLeftTrue val = refl

That doesn't work because of a type-mismatch, so replacing the predicate through substitution eventually lead to this type-error:

When elaborating right hand side of isEqLeftTrue:

Can't unify
x = x
with
(val : a) -> val == val = True

See, the problem (or, more correctly: my problem) is that

val == val 

is true, but that's a property of boolean decidability, perhaps? It's easy enough to solve if I refine the term

val == val 

down to

True

then apply the reflexive property to obtain my proof, but the problem (again: my problem) is that I'm not all that savvy with refinement in proofs to get the answer out and blogged today.

The show must go on!

But the co-problem, or, getting a little less esoteric, the solution is that the Idris language already provides something that addresses this: so

Idris*> :t so
Prelude.Bool.so : Bool -> Type

With so we say that something is true, typefully, (that's a word, now) for us to proceed. So, our isEqLeftTrue, etc, functions become easy to write:

isEqLeftTrue : Eq a => (val : a) 
-> so (leftIsomorphism (True, val)) -> ()
isEqLeftTrue val pred = ()

and then verification is simply the compilation unit, but you can query the type or test out any value with it as well:

Idris*> isEqLeftTrue "hey"
isEqLeftTrue "hey" : (so True) -> ()

And there you go, we've verified, for the left-adjoin anyway, that a (,) True type has the identity function. Let's verify the other three cases as well:

isEqLeftFalse : Eq a => (val : a) 
-> so (leftIsomorphism (False, val)) -> ()
isEqLeftFalse val p = ()

... and for our right-adjoin proofs:

rightIsomorphism : Eq a => Either a a -> Bool
rightIsomorphism eith = (g . f) eith == eith

isEqRightLeft : Eq a => (val : a) 
-> so (rightIsomorphism (Left val)) -> ()
isEqRightLeft val p = ()

isEqRightRight : Eq a => (val : a) 
-> so (rightIsomorphism (Right val)) -> ()
isEqRightRight val p = ()

... and then the compilation proves the point, but we can exercise them, as well:

Idris*> isEqLeftFalse 1

isEqLeftFalse 1 : (so True) -> ()

Idris*> isEqRightLeft 'a'

isEqRightLeft 'a' : (so True) -> ()

Idris*> isEqRightRight "hey"

isEqRightRight "hey" : (so True) -> ()

... and there you have it.

Pensée

Huh. Looking at the above four proof-functions, they have the same type signatures (pretty much) and the same definitions. Hm. Maybe that's an indicator for me to start looking at Idris' syntactic extensions? Something for me to pensée about.

Ciao for now.

'Z' is for the ζ-calculus

'Z' is for ζ-calculus  (pronounced 'zeta-calculus')

So, 'Z' is the last letter of the alphabet, unless you're Greek, then ζ is the sixth letter. The last letter of the Greek alphabet is Ω.

But we already did Ωm-Ωm-Ωm. Ram-Ram-Sita-Ram-Sita-Ram-Ram, so we're good there.

As α denotes the beginning of things, Ω (which on a Mac, you get by selecting option-Z. Fitting, that) denotes the end of things. That's why everybody back then got it when Jesus said: "I am the α and the Ω."

He was the package deal.

But look at you all, doing your A-to-Z challenge faithfully. Did you survive? Are you shell-shocked?

To put this into perspective, my mom was a journalist for local news for our local newspaper. She did the A-to-Z challenge, every day (except Sundays), every month, year-after-year.

So you've completed your A-to-Z challenge. Congratulations! Now, lather, rinse, repeat, every month, for the rest of your life, right?

And you thought one month was hard?

Okay, last entry for my A-to-Z guide book for surveyists, explorers and tourists of mathematics.

Okay, so the lambda calculus is the commingling of the κ-calculus (the contextual calculus) and the ζ-calculus (the control calculus), which we talk about in this post (disclaimer/citation: I get most of my information on the ζ-calculus from Hasegawa's seminal 1995 paper on the κζ-calculi). A good deal of attention, when it has been given at all, has been focused principally on the κ-calculus...

'And why not!' says most. In the κ-calculus you get things done. There's no application, but through composition of (first-order) functions and first-order tuple-types you have numbers, counting, addition, and all the rest come out of that.

With the control calculus you make functions that take functions as arguments.

τ : 1 | ((—) ↠ (—))

So reduction (to your answer) is of the form of the continuation-passing form, for a function in the ζ-calculus f : a → b is of the ζ-term form of:

ζ f : a → (c ↠ b)

Which is to say, the zeta-term, f, take a functionally-typed argument, a, and returns the continuation (c ↠ b).

Now, we got the κ-calculus to work by lifting function arguments to tupled-typed terms, and we saw that with the implementation of addition (here). Now, instead of lifting unit types to tuples, in the ζ-calculus we pass a function on x to the zeta-term by using functional composition, i.e.:

pass(c) o (ζ x . f) ~> f[c/x]

To be able to construct a function in the ζ-calculus we have the function-constructor, code:

given f : c → d and x is the 'constifying function' : 1 → c

we have f o x : 1 → d

from that we have code:

code(f) ≡ ζ x . (f o x) : 1 → (c ↠ d)

Boom! code, then, is a function that creates a function from nothing (the '1' type).

But, okay, what can you do with the ζ-calculus?

Well, since we don't have unit cartesian types, like we have in the κ-calculus, then the answer to that is, well, ... nothing, really.

I mean, it's possible to have function represent unit types then start composing them to build an algebra, but this approach is rather unwieldy. The ζ-calculus exists to show that the λ-calculus is perfectly decomposable into the κ-calculus and the ζ-calculus, and so control is usually mapped out in the ζ-calculus (although some directed flow is possible in the κ-calculus, itself alone, as we've seen) (link).

For example, to create the numbers zero and one are possible in the ζ-calculus, but when we try to represent two (that is, functionally, double application), we get this:

x : 1 → c

z : 1 → (c ↠ c)  pass(x) : (c ↠ c) → c

  pass(x) o z : 1 → c  -- so we've got our constant continuation (step 1)

pass(pass(x) o z) : c ↠ (c → c) -- now we've got a continuation-creator

pass(pass(x) o z) o z) : 1 → c

ζx (pass (pass(x) o z) o z) : 1 → (c ↠ c) -- continuation-creator for the right-hand side

dupl ≡ ζz . ζx (pass (pass(x) o z) o z))) : 1 → ((c ↠ c) ↠ (c ↠ c))

And there we have it, the dupl(icate) function, or the number two, in the ζ-calculus.

Ugh!

Well, you did say you wanted to see it. I did, too. It's a morbid fascination of mine, watching this train wreck transpire.

The Takeaway here

But that's a reveal. Math isn't necessarily easy (shocker!) nor is it necessarily neat. Here we see in the ζ-calculus that it's difficult to express things (like, for example, the number two, or any unit types).

So, if you've got a correspondence (a provable one), all you have to do is to change categories to one where you can express what you need to simply and cleanly.

The application works here, and now, too.

I'm doing things slow and stupid, because I'm doing them the way I've always done them, the way I see how they're done.

Change categories. Somebody is doing what I'm doing, but doing it well. Somebody isn't doing what I'm doing, because they've moved onto better things — more sublime problems — ... I can do the same thing. All I have to do is change my perspective, how I see things, and then, seeing them anew, I can do what I need to do, what I want to do, simply and cleanly, then translate back down to the way I always do things, ...

Or hey, just move on, after having moved up.

It's called a 'lifting function.' It lifts an object from one category to another one, and in being lifted, the object is changed, and what it can do (its morphisms) are changed. And you can change it back 'down' (the co-ajoint function) or you can stay in the newly-lifted category, or you can lift again.

Math is neat that way, once you see that as a possibility.

Life can be like that, too.

Life is neat that way, once you see that as a possibility.

'Z' is for the ζ-calculus.

And with 'Z' we're all done doing our A-to-Z petit survey of mathematics and logic. I hope you had fun, for I had a blast writing these posts.

Thank you for reading them.

'K' is for Kappa-calculus

'K' is for κ-calculus

This is an epic story of epic epicness!

No, really.

So, way back when, this guy named Church (Alonzo was his Christian name, and he liked going to churches)

(Actually, that's just conjecture on my part.)

Okay, everybody, stop everything and go to this wikipedia link on the Frege-Church ontology, right now.

Have you read it?

Well, what are you waiting for, read the post, for goodness sake!

I'M WAITING!

...

Okay.

So, I read the post, and I was all like skyr, you know? No whey!

Like, totally! Like. I mean, like, wikipedia, wrote that?

So, I quizzed my girls:

"Girls!" I shouted excitedly, "What's the farthest planet from the Sun?"

They were like, "Whaaaaa?"

Then they asked, like, "Papa!" with arched eyebrows, "why do you want to know what's the farthest plant from the Sun?"

Hm. I, like, have to work on my, like, diction.

(We'll get to the reason behind the paroxysms of 'like's momentarily.)

So, I clarified, "Planet, planet!" I shouted, "What's the farthest planet from the Sun!"

EM, the older, and therefore smarter one (she has to be, you see), said, "Pluto. No, wait. Pluto's not a planet. Neptune, then!"

"HAAAAAA!" I screamed.

Elena Marie looked at me like her Papa had finally gone off the deep end.

Well, finally off the deep end, but this time, never to return, gone-off-the-deep kind-of-way.

But before I could explain my victorious berserker scream ...

(Berserker, n.: etymology: íslandic, "Bear Skinned")

(Question: what is the etymology of the word 'etymology'?)

(Did you know Icelandic is an insular Nordic language? They can read the poetic and prose eddas straight off, just like that. Could you read a 1,000 year old document? No, you can't, unless your an Icelander. So there.)

(But I digress.)

(As always.)

(The neat thing here, is this is a digression, from a digression! And it's not even leading us back to the topic, but further away) (just as this digressionary turn discussing my digressionary habits).

(Digressions within digressions within digressions.) (Move over, Frank Herbert, you dead old guy, you're not the only one who can write 'Wheels within wheels within wheels' and have a really bad movie with a Sting cameo made out of your book!)

BUT BEFORE I COULD EXPLAIN my berserker-scream, Li'l Iz piped right up.

"How can you know what's the farthest planet of the Sun, huh, Papa? There're other planets in this galaxy, and what about other galaxies, huh?"

She had me there. But never confuse the point you're trying to make with facts.

WHEN I REREAD what I wrote to my girls, they sighed, appreciatively, EM said, "How ironic can that be?" and walked off to her room to read another book before her ballet recital in forty-five minutes.

I asked Li'l Iz, "Was that, like, ironic?"

She rolled her eyes and deigned not to answer, returning to her own book.

SO, the POINT of all this is:

Pluto is not a planet!

Whew!

I'm so glad that the ravings of a madman in Borderlands 2 would actually have significance to mathematical logic theory. The things one learns by reading blogposts by the geophfmeister.

(That is moi-self) (That is French) (No, it's not.)

Ooh! Digression!

When I was working with some Ph.D.'s and cognitive scientists, I worked with this flaming-red-haired dude (cognitive scientist) named Bill. He would always say 'Gratzi' to people answering his questions, I would always respond: "That is French."

He always gave me weird looks, but he never got the nerve to correct me.

Until one day, he said 'Gratzi' to one of our analysts, and I said, 'That is French.'

She looked me dead in the eye and snarled a disdainful, "Who cares?" before stalking off.

Bill was on the floor, suffering a paroxysm of laugher.

I think that was the best day of his life.

ANYWAY!

Pluto, not planet ... It's not even a plant.

Besides which, Eris is more massive than Pluto, anyway. So there.

Hail, Eris!

SO!

The Lambda calculus ('L' is for Lambda calculus) addressed a certain set of concerns, which I'll get to in Monday's post, but it, like mathematics in general, has its own set of problems, that is, you can write a function that never terminates and so it is undecidable.

So, along came this little kid by the name of Masahito Hasegawa (dunno, maybe he's Italian?) and he noticed something, and that was this: the problem of the lambda calculus is that it's actually two calculi intertwined. And when you disentangle them, you have two distinct calculi, neither of which are undecidable.

The first of the calculi, the one we focus on here, is the κ-calculus, or contextual calculus.

The κ-calculus is this.

The types are pairs of unit types:

τ : 1|τ x τ|...

So, you see from the types that it's either nothing (the 1, or unit type) or it's a (crossed, or cartesian product) of types.

The functions only take these types, NOT functional types, so we're safe in that we're only working with unit types.

The primary operation is the lifting function, which takes an instance and lifts it into the type of concern.

liftτ x -> (a, x) where a is of type τ

Then the κ-abstraction that when acting with an instance carries it along:

κ x . (some function (τ1, τ2) -> τ3) : τ3

Tying lift and the κ-abstraction together gives us our function 'application' where actually no application happens, it's all just composing (in this case) tuples.

'F' is for function

'F' is for function.

Okay, you just knew we were going there today, didn't you?

Today, and ... well, every day in the last 2,600 years (I'm not joking) has had this dynamic tension between objects and functions. Which is greater?

Read this tell-all post to find out!

Sorry, I channeled Carl Sagan in Cosmos for a second. 

Not really.

But I digress.

WAY back when, back in the olden times, there were just things, and then when you had a full belly and your one thing, your neighbor, who happened to be named 'Jones,' had two things.

And then keeping up with the Jones' came to be a real problem, because you had one thing, and they had two. So you got one more.

And counting was invented.

For things.

In fact, in some cultures, counting doesn't exist as an abstract thing. You don't count, in general, you have different counting systems for different things. Counting, for example, pens, is a very different thing than counting eggs.

Ha-ha, so quaint! Who would ever do that?

Well, you do. What time is it? You have a different way for counting time than you do for counting distance or for counting groceries that you need to buy, don't you?

But, at base, they are all just things: time, distance, and gallons of milk.

Sorry: litres of milk. How very British Imperial of me!

Question: why are Americans just about the only ones using the British Imperial system any more? That is, the real question is: why are the British not using the British Imperial system? They onto something we're not?

Anybody want a satellite coded wrongly because some engineers intermingled British Imperial units with metrics?

Okay, so, units, things, metrics, whatevs.

And counting.

Counting is doing something to something, whereas, at first, it's important you have that chicken in your stomach (cooked is nice, but optional), suddenly it's become important that you have not one chicken, a hen, but a (very rarely) occasional rooster with all your hens would be nice, too.

(Roosters are big jerks, by the way.)

Counting was all we had, after the chickens and their yummy eggs, that is, and that for a long while.

Question: which came first, the chicken or the egg.

Answer: that's obvious, the egg.

Think about it. You have eggs for breakfast, then you have a chicken-salad sandwich.

Like I said: obvious! First the egg, then the chicken.

Unless you're one of those weirdos that eat chicken sausage with your breakfast, then it's a toss-up, but in that case I have no help for you.

Okay, chickens, eggs (egg came first) (You read that first, right here on this blog) (and you thought there was no point to math!), and then counting, for a long, long time.

Then, ... counting became too much, because you ran out of fingers, then toes, to count your mutton on. It happens. That's a good thing, because then people started to have to think (that's a good thing, too), and they thought, 'how do I count all my mutton when I run out of fingers and toes? I need to know that I have more sheep than the Jones', and I've paired each of my sheep to his, and I have more than twenty-two than he does. How many more do I have!"

Then people started getting smart. They did more than one-to-one, or pairwise, groupings, they started grouping numbers, themselves.

All this is very nice background, geophf, but to what end?

First counting, then grouping, those are operations, and on or using numbers.

Then addition and subtraction, which are abstractions, or generalizations on counting, then multiplication, and let's not even go into division.

But.

Counting, adding, multiplying. These things worked for you chickens (and eggs) (first), but also on your mutton, and when you settled down, it worked on how many feet, yards, the hectares of land you had, too. The same principles applied: numbers worked on things, no matter what the things were, and the operations on numbers worked on ... well, no matter what the numbers counted.

Now. Today.

Or, sometime back in the 40s anyway, way back before the Birkenstock-wearers were mellowing out with lattes, anyway. A couple of dudes (Samuel Eilenberg and Saunders Mac Lane, specifically) said, 'Hey, wait!' they exclaimed, 'it doesn't matter what the thing is, at all!' they said, 'as long as the things are all the same thing, we don't care all all about the thing itself at all!'

And they invented a little something that eventually became known as Category Theory, which is the basis of ... well, a lot of things now: quantum thermodynamics, for one, and computer science, for another.

And they nailed it. They created a one-to-one correspondence between the things in categories and the things in Set theory.

Why is that important? Set theory is this:

{}

Got me?

A set is a thing that contains a thing. The fundamental set is the set that contains nothing (the 'empty set'), which is this:

{}

And other sets are sets that contain sets:

{{}, {{}, {{}, {}}}}

With sets you can model numbers if you'd like:

0: {},

1 {{}} (the set that contains '0'), 

2: {{}, {{}}} (the set that contains '0' and '1')

3: {{}, {{}}, {{}, {{}}}} (the set that contains '0', '1', and '2')

etc...

And as Gödel (eventually) showed, once you model numbers, you can model anything.

(We'll get to that ... for 'G' is for Gödel-numbering, I'm thinking)

How? Well, once you have numbers, you can count with them (as just demonstrated), you can add one to them (the 'successor' function), you can take away one from the (the 'predecessor' function), you can add two of them together (successively add one to the first number until the second number is zero. Try it!), subtract, by doing the opposite (or by just removing duplicates from both until one of them is gone ... 'pairwise-subtraction'!), multiply two together (successive addition), divide numbers ... (um, yeah)... and, well, do anything with them.

Once you have Number, you have counting, and from that, you have everything else.

So, our dudes mapped category theory things (morphisms) down to Set mapping functions, and they had it.

Because why?

Well, it's rather cumbersome to carry a whole bunch of sets for your Pert formulation, especially when you want to see the money you (don't) save by paying off your mortgage's principal early.

Banker: oh, geophf, pay off your mortgage principal early, you'll save a ton in the long run.

me: uh, that was true when mortgage interest was 10-15-21%...

(you remember those Jimmy Carter days?)

me, continuing: ... but now that my interest rate is 2.5% I save zip after 30 years for early payment.

Try it. Run the numbers. Bankers haven't. They're just repeating what was good advice, ... twenty-five years ago.

But when you have objects, whose representations do not matter, be they 0, 1, a googol, or {{}, {{}}, {{}, {{}}}}, then you can concentrate on what's really important.

The functions.

Whoopsie! I slipped and gave the answer, didn't I?

Me, and Alan Kay, both.

Alan Kay, inventor of Smalltalk, and inspirer of the movie Tron: The objects aren't important, it's the messages that go between them that is.

So there.

Well, okay, functions win. It used to be the chicken (or the egg), but now we've ... grown a bit, worrying less about what fills our stomach, and where we're going to get our next meal (and not be the next meal), you know: survival.

We've transcended our stomachs.

Maybe.

Well, okay, functions rule, so back off.

The dudes didn't stop there, because there's been some really neat things going on with functions, since discovering functions are things in and of themselves, because if functions are things, in and of themselves, then, well, ...

Well, you can number them (tomorrow) (promise), you can count them, you can add them, you can multiply them, you can exponate them, you can ...

You can, in fact, operate on them, applying functions to functions.

So, our dudes did just that. They said their functions, their morphisms have two rules to be a function.

You can ask what it is, it's identity:

id f = f

And you can string them together, composing them:

g . f = ... well, g . f

So, if you have 

> f x = succ x

and 

> g x = x * 2

then (g . f) gives you some function, we can call it, h, here if you'd like, and h is the composition of applying f to your number first, then g, or

> h x = 2 (x + 1)

Try it!

Pull up your functional programming language listener (I use Haskell for now) (until I find or invent something better)

and enter the above.

Now, it's an interesting proposition to show that

(g . f) == h

But, for now, in Haskell, we cannot do that.

Now, in some other programming languages (I'm thinking of my experience with Twelf), you can, but first you have to provide numbers, on you own, like: 0, 1, 2, ...

... and prove they are what they are, you know: they follow in order, and stuff like that ...

Then you provide the functions for identity and composition, and then you can prove the above statement, because now you have theorems and a theorem prover.

Yay!

No, ... no 'yay'!

I mean, 'yay,' if that's your thing, proving theorems (I happen to have fun doing that at times), but 'ick,' otherwise, because it's a lot of work to get to things like just plain old addition.

See, theorem-prover-folk are these hard-core fighters, right on the edge of discovering new mathematics and science. Not plain-old-little me, I just use the stuff (to build new theories from preexisting, proved, ones), so I'm a lover of the stuff.

To quote an eminent mathematical philosopher: I'm a lover, not a fighter.

And, no, Billie-Jean is not my lover. She's just a girl that claims that I am the one.

Anyway!

So, but anyway, using the above two functions, identity and composition, you're now able to reason about functions generally, making new functions by stringing together (composing) other, preexisting functions.

This is so important that Eilenberg and Mac Lane gave this process it's own name 'natural transformation.'

But okay, Categories have units and you don't particularly care what those units are; we saw one set of units, numbers, themselves, as an example,

But units can be anything.

Even functions, so you have a category of functions (several categories, in fact, as there are different kinds of functions, just so you know) ... You can even have categories of categories of things (things being some arbitary unitary types, like numbers, or functions, or categories, again ... it can get as wild and woolly as you want it to get).

And types. Categories can be used to model types, so you can have a category that represents the natural numbers ... as types:

Nat : Category

zero : 1 -> Nat

succ : Nat -> Nat

so zero = zero ()

one = succ zero ()

two = succ one

three = succ two

etc ...

And those formula, those functions works, regardless of the underlying type of things like 'number' or even 'function.'

Category theory was originally called 'Abstract nonsense,' by the way, because Eilenberg and Mac Lane saw it as so abstract that they were actually talking about nothing.

Sort of like how Set Theory does, starting from nothing, the empty set, and building everything from that object, but even more abstractly than that, because category theory doesn't even have the 'nothing'-object to start from, it just starts identifying and composing functions against objects about which it doesn't care what they are.

Now, there was, at one point, a working definition of abstraction, and that was: the more useful a theorem is, the less abstract it is.

The contrapositive implied: the more abstract a formula is, the less useful.

But I find I play in these domains very happily, and in playing, I'm able to invent stuff, useful stuff that's able to do things, in software, that other software engineers struggle with and even give up, stating: "This can't be done."

I love it when I'm told I "can't" do something.

You know what I hear when I hear the word "can't"?

I hear opportunity. 

Everyone else may have given up on this particular task, because it 'can't' be done. But me? I go right in with my little abstract nonsense, reinventing the language that was unable to frame the problem before with a language that can, and I find, hey, I not only can do it, but I just did.

Language frames our thoughts, telling us what we can and cannot do. English is a very complex language, taking in a lot of the world and describing it just so.

The language of mathematics is very, very simple, and describes a very tiny world, a world that is so tiny, in fact, doesn't exist in reality. It's a quantum-sized world: mathematics and has the possibility to be even smaller than that.

But so what? I get to invent a world that doesn't exist, each time I apply a theorem from mathematics that others are unfamiliar with.

And when I do so, I get to create a world where the impossible is possible.

It's very liberating, being able to do things others 'can't.' And when I pull it off, not only do I win, but my customers win, and maybe even those developers who 'can't' win, too, if they're willing to open their eyes to see possibilities they didn't see before.

'F' is for functions, a totally different way of seeing the world, not as a world of objects, but as a world of possibilities to explore.