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.

'T' is for Theorem-proving

'T' is for Theorem-proving

So, you've been theorem-proving all your life.

Let's just get that one out there.

When you're given a math problem that says:

"Solve x + 1 = 2 (for x) (of course)"

And you say, "Why, x is 1, of course," quick as thinking, you've just proved a theorem.

Here, let me show you:

x + 1 = 2 (basis)

     -1 = -1 (reflexive)

x + 0 = 1 (addition)

x       = 1 (identity)

Q.E.D. ('cause you rock)

So, yeah. Theorem proving is this, correction: theorem proving is simply this: going from step 1, to step 2 to step 3 until you've got to where you want to be.

How do you go from step 1 to step 2, etc? The same way you do everything! You follow the rules you're given.

Let's prove a theorem, right now.

So, in classical logic, we have a theorem that says

p → p

That is, if you've got a p, that implies (that you've got a) p.

Toughie!

But proving that? How do we go about doing that?

Well, in classical logic, you're given three basic axioms (thanks to sigfpe for his article "Adventures in Classic Land"):

1. p → (q → p)

2. (p → (q → r)) → ((p → q) → (p → r))

3. ¬¬p → p

So, p → p. How do we get there? Let's start with axiom 1 above.

1. p → ((p → p) → p)

axiom 1 (where q = (p → p))

2. (p → ((p → p) → p) → ((p → (p → p)) → (p → p))

axiom 2 (where q = (p → p) and r = p)

3. (p → (p → p)) → (p → p)

modus ponens

4. p → (p → p)

axiom 1 (where q = p)

5. p → p

modus ponens

Q.E.D. (a.k.a. whew!)

I used something called modus ponens in the above proof. It says, basically, that if you've proved something that you're depending on, you can drop it. Or, logically:

p → q, p

       ∴ q

Or, we have "p implies q" we've proved p, so now we can just use q.

Now, there's been a lot of thought put into theory, coming up with theorems and proving them, and this has been over a long time, from Aristotle up to now. The big question for a long time was that ...

Well, theorem proving is a lot of hard work. Is there any way to automate it?

So there's been this quest to make theorem proving mechanical.

But to make theorem-proving mechanical, you have to mechanize everything, the axioms, the rules, and the process. Up until recent history, theory has been a lot of great minds spouting truths, and 'oh, here's a new way to look at the world!'

And that has been great (it has), but it hasn't helped mechanize things.

Then along came Frege. What Frege did was to give us a set of symbols that represented logical connectives and then symbols that represented things.

And there you had it: when you have objects and their relations, you have an ontology, a knowledge-base. Frege provided the tools to represent knowledge as discreet things that could be manipulated by following the rules of the (symbolized) relations.

He gave abstraction to knowledge and an uniform way of manipulating those abstractions, so, regardless of the underlying knowledge be it about money or chickens or knowledge, itself, it could be represented and then manipulated.

That way you could go from step 1 to step 2 to step 3, etc, until you arrived at your conclusion, or, just as importantly, arrived at a conclusion (including one that might possibly say what you were trying to prove was inadmissible).

Since Frege, there has been (a lot of) refinement to his system, but we've been using his system since because it works so well. He was the one who came up with the concept of types ('T' is for Types) and from that we've improved logic to be able to deliver this blog post to you on a laptop that is, at base, a pile of sand that constantly proving theorems in a descendent of Frege's logic.

Let's take a look at one such mechanized system. It's a Logic Framework, and is called tweLF. The first example proof from the Princeton team that uses this system is 'implies true,' and it goes like this:

imp_true: pf B -> pf (A imp B) = ...

That's the declaration. It's saying: the proof of B, or pf B, implies the proof of A implies B, or pf (A imp B).

How can you claim such a thing?

Well, you prove it.

imp_true: pf B -> pf (A imp B) =

[p1: pf B]            % you have the proof of B

% ... but now what? for we don't have the proof that A implies B

.

So the 'now what' is our theorem-proving adventure. Mechanized.

We don't have the proof that A implies B, but we have a logical loop-hole (called a hole) that a proof some something that's true is its proof:

hole: {C} pf C.

Which says, mechanized what I just said in words, so with that:

imp_true: pf B -> pf (A imp B) =

[p1: pf B]

(hole (A imp B)).

And there you go.

... that is, if you're fine with a big, gaping loophole in your proof of such a thing.

If you are satisfied, then, well, here, sit on this rusty nail until you get unsatisfied.

So there.

Okay, so we have an implication, but we need to prove that.

So we introduce the implication into the proof, which is defined as:

imp_i: (pf A -> pf B) -> pf (A imp B)

SO! we have that, and can use it:

imp_true: pf B -> pf (A imp B) =

[p1 : pf B]

(imp_i ([p2: pf A] (hole B))).

So, we have the proof of A and that leads to B. But wait! We already have B, don't we? It's p1 (that is [p1 : pf B])

BAM!

imp_true: pf B -> pf (A imp B) =

[p1 : pf B]

(imp_i ([p2 : pf A] p1)).

DONE!

This is what theorem-proving is: you start with what you want, e.g.:

imp_true: pf B -> pf (A imp B)

which is "implies-true is that if you have B proved, then you have the proof that (A implies B) is true, too."

Then you take what you've got:

pf B

And give it a value:

[p1 : pf B]

Then you apply your rules (in this case, implication introduction, or 'imp_i') to fill the holes in your proof, to get:

[p1: pf B] (imp_i [p2: pf A] p1)

Which is the demonstration of your proof, and that's why we say 'Q.E.D.' or 'quod est demonstratum.' 'Thus it is demonstrated.'

Ta-dah! Now you have all the tools you need to prove theorems.

Now go prove Fermat's Last Theorem.

eheh.

(I am so mean!)

Okay, okay, so maybe Fermat's Last Theorem is a bit much, but if you want to try your hand at proving some theorems, there's a list of some simple theorems to prove.

'H' is G++

'H' is 'G'++

(Mathematical humor ... gotta love it!)

(although the symbol '++' to signify 'Mathematical Humor' is an egregious misnomer, as the 'auto-increment' operator is not mathematical in any sense at all! How do you auto-increment the number 4 to become the number 5? You don't!)

(So there.)

(Not that I'm digressing or anything, but ...)

(continuing right along from the previous post, la-di-dah, as if I didn't fall asleep right on my laptop, or anything like that) ... to get there, but now we enhance Gödel translation functions, instead of translating ⊥ (the uninhabited type), we instead choose some (arbitrary) type, k, to be translated and then to do our translation:

k^⊥ -> k

(p -> q)^k -> (p^k -> q^k)

The beauty of this is that k, our arbitrary type, can be anything we choose, be it integers or person-objects, or whatever unit of logic we are having the conversation about.

We can now lift the conversation from classical logic to intuitionistic logic, because we now have a translation for 'not' that intuitionistic logic can deal with, and that is:

¬p == p -> ⊥

Now, translating from intuitionistic logic to executable (programming) code, that's been covered in the literature by other articles, ... maybe I'll take that under 'i' for intuitionistic logic or 't' for program translation, but not here.

Epilogue

As promised, the Gödel numbering.

There's actually many ways to skin this Schödinger's cat. One of them, not Gödel's, is to recode what is a 'number.'

For example, in the programming language Forth, at base 36, every number, and letter, is a number!

0 is 0

1 is 1

...

9 is 9

A is 10

B is 11

...

Z is 36

There it is: base thirty-six. In base thirty-six, the number 'number' is

foldr (\c sum -> sum * 36 + ord c - ord 'a' + 10) 0 "number"

or 1656644207.

Huh. A pretty big number.

So one encoding is to assign primitive functions to numbers (which now include letters) and when we string them together we have an unique number for each formula,

So, if we give

B

the value

B = \x y z -> x(yz)

And

C

the value

C = \x y z -> xzy

and

I

the value

I = \x -> x

and

K

the value

K = \x y -> x

and

M

the value

M = \x -> xx

and

S

the value

S = \x y z -> xy(xz)

We can actually write statements of truth using these letters, like:

SKK

or

M(KBC(SI)(KSK))

or

... anything else

(you see a problem, however: I did have to use open and close parentheses, so those two symbols must also be introduced as numbers).

And the above formula are actually numbers as well as being formulae, that is statements of truth, that can be reasoned about.

That's one numbering; the alphabet-soup that Combinator logic is.

Another is even simpler, reducing down to the simplest pair of combinators (including parenthesization (that, actually, is a word, regardless of what my stupid spell-checker says.) (stupid spell-checker)), and for that we have the iota programming language, or just ι to its friends.

Programs look like this in ι:

1011110110111101

Needless to say, that, too, can be reduced to a number which can be reasoned about.

Gödel went in neither of these directions, or, instead of looking at a functional/lambda approach, he chose to represent mathematical logic in ordinal form, and instead of using combinators to eliminate variable-representation from his statements, he also represented logical variables in his enumerated set of symbols,(1) choosing a basic set of logical symbols to represent as numbers, so each number became, not a function, but a statement of truth.

He would encode a statement of truth by it's (lexical) ordering, so:

¬¬p

if ¬ were encoded as 1 and 'p' were encoded as 2 would be represented as powers of primes:

2¹ * 3¹ * 5²

And by the fundamental theorem of algebra, the resulting number, for an unique input statement would yield an unique number.

Coolness!

But how do you represent numbers here?

Gödel used Peano numbers, which, like the Roman numerals, are unary:

z = 0

sz = 1

ssz = 2

sssz = 3

... you get the point

So if 'z' is 3 and 's' is 4

Then the number 12 is 12 s's followed by a 'z' which is

2³ * 3³ * 5³ * .... * 41⁴ 

which is number so big that if I had a dollar for every 's' in its resulting Peano representation, ... well, I'd have a lot of dollars!(2)

Well, so using simple logic symbols (that created very, very, ... very big numbers) (bigger than infinity + 1, even!) (Okay, now I have to go to confession), Gödel was able to create a predicate that determined if a formula was determinable in Principia Mathematica, he named it det(f) ... I suppose because 'Gertrude' was taken, already, so he had to settle for 'det.'

It also could be because 'det' implies 'determinable,' and not because of unrequited love, but mathematicians' hearts are always breaking over a girl named Agatha (just ask one of the world's most famous mathematicians, I'm sure you've heard his name: Brahms. Johannes to his buddies) or Gertrude or Millicent or Chrysanthemum.

Ah, Chrysanthemum!

But I digress.

So, but what happens when you run a formula that never returns through det?

For example, the formula M is \x -> x x, so the formula M M reduces as follows:

M M -> (\x -> x x) M -> substitute M in x gets you M M -> (\x -> x x) M -> substitute ... forever.

M M gets you M M and when you try to reduce that it gets you M M.

M is known as the looping function. It gives you loops, functionally, or drives you loopy.

Either one. Or both.

So, the point is that det(M M) is ...

There is no answer to that.

And that's the problem, because now you have a case were det itself is ... wait for it.

Not det.

det is not det.

That's like saying p = ¬p or 5 isn't 5 anymore.

That's inconsistent.

Once Gödel had that, he encoded det as a Gödel number (it was 'rather' large)(like: infinity + 2)(... but not) and then showed that ¬ det(det) was true inside the Principia Mathematica, and using only the axioms and rules that the Principia Mathematica allowed.

The Principia Mathematica, a system Russell created and worked so hard to show was complete and consistent ...

Well, Gödel showed that it was inconsistent, and showed it entirely within the Principia Mathematica framework.

That show, that proof, was named Gödel's Incompleteness Theorem (again, because Gertrude was taken, at the time), and has forever changed the tenor and tone of the conversation of mathematics since.

Meta-epilogue: 'H' is for Hilbert

Now I was going to go on a rant about how ++ is just plain bad in every sense of the word. Once you can change the number 5 into the number 6, then you have just opened up a box that you can never close again.

In Category Theory a function has identity and composition, but if you can change something, anything, like, the function, then what does identity mean? ('I' is for isomorphism. But later, not now).

Identity loses its meaning in the face of mutability, and provable properties about your theories and your system at large go out the window.

But I not going to talk about 'H' is for G++ and how mutability is just plain bad, bad, bad.

I'm not.

I'm going to talk a little bit about Hilbert.

Okay, so this dude was on fire. He basically invented mathematical logic, as a concept, and stood up before the whole world and held in his hands the only set of unsolved problems in math (there were 23 of them) and he shook his fist and said the famous last words: "We must know. We will know!"

Then he died. Then Gödel proved mathematics inconsistent, intrinsically so.

Not only that, Gödel, and others using his work, showed at least three of the problems were unsolvable. It wasn't that the solution was hard to get to without computers or supercomputers (that they didn't have at the time) nor even quantum computers ('Q' is for qubit) (later! later!) but they were intrinsically unsolvable because of Gödel's incompleteness theorem.

Bam.

Poor Hilbert!

I mean, he died brimming with hope. He had his words carved on his gravestone: "We must know. We will know."

And now, we will never, ever will know.

'H' is for Hilbert. He thought we were big enough to conquer all of mathematics.

But they did name Hilbert-space after him. So he does have that going for him.

-----

Endnotes:

(1) This smacks of coding in the good old days of FORTRAN where you could have any integral variable you wanted, insofar it was named either 'i' or 'j' or 'k' ... what? You want more variables? Go write a different program! Jeez! Why would anybody want a variable named something else than i, j, or k, anyway!

(2) 1154720154130223108008498916387587352955801000 of them, in fact! I'd buy that for a dollar!