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*looks exactly like

^{T }*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*? We get this:

^{K}*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*

*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.*

*g*∘

^{K}

^{K}*f*⇒

^{K }*A*→

*T B*→

*T C*

**Practical Application**

*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.

*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.

*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.

**Summary**

## No comments:

Post a Comment