[Experimental] Compiling Scala into Closed Cartesian Categories language using ScalaFix rewriter
The idea in this post is to experiment about compiling Scala code into the internal language of Closed Cartesian Categories “CCC” (as expressed by Curry-Howard-Lambek isomorphism). But we want to perform this translation into CCC language within Scala itself and then run this program in the context of another category than the simply-typed lambda category you all know. For simplification, we limit the Scala code to simple lambda expressions on numerics or booleans. Finally, we’ll show how we can translate Scala code at compile-time into CCC language using ScalaFix/ScalaMeta tooling.
This idea is not mine at all but the one of Conal Elliott (and certainly others) that he’s presented in multiple Haskell posts, talks & specially this paper http://conal.net/papers/compiling-to-categories/compiling-to-categories.pdf. Haskell is much nearer from 𝛌.calculus than Scala and his code samples in Haskell are often shorter & clearer but I’ll focus on Scala code for this experimentation and also because there are not so many posts about this topic in Scala.
I’m not a mathematician so I might be mathematically imprecise sometimes so don’t hesitate to tell me if I write true horrors. My aim is just to explain as clearly as possible & make people aware about those concepts.
“Part1— From CHL isomorphism to CCC language in Scala” is a long step by step explanations trying to put words on those abstract things for those who don’t really know.
“Part2 — Compiling primitive function to CCC in Scala” is where you need to know a bit what CCC is.
Part1 — From CHL isomorphism to CCC language in Scala
Curry-Howard-Lambek isomorphism, you know it, right? You heard the 2 first names at least once if you’re looking at Types & Functional Programming. The 3rd name is not so well known. I think we could add many other names to this list because this idea has been studied by so many people.
To extend Harper’s idea about “computational trinitarianism”, let say Curry-Howard-Lambek correspondence expresses one of those mathematical trinitarianisms: 3 distinct concepts seen from 3 different mathematical points of view, representing one single substance, essence or nature or concept or thing or “truc” as we say in French.
I said “one of those trinitarianisms” because IMHO, in mathematics, there is not one single trinitas but many trinitates or homoousianisms or consubstantialisms depending on your jargon (nice words, aren’t they?)… Even n-itates … An infinity of them actually. It’s the nature of mathematics to consider concepts from many different angles and draw bridges between different points of view.
So, this CHL correspondence tells us that the 3 following things are the same:
- Types & terms from the simply typed 𝛌.calculus (Church created in ~1940)
- Proofs & propositions from intuitionistic logic (link with 𝛌.calculus established in ~1930–40 by Curry and then ~1960–1970 by Curry/Howard)
- Objects & morphisms from closed cartesian categories (link with 𝛌.calculus established by Lambek in ~1970–1980)
Simply typed 𝛌.calculus is part of your everyday life as soon as you build a program and use functions with typed inputs & outputs and variables. Any typed functional language like Haskell, ML (and even Scala) is based on it, more or less closer, just adding a few more concepts on top of it like products, coproducts, recursion, polymorphism, higher-order abstractions etc…
Intuitionistic Logic is also part of your everyday life as soon as you use your brain for any reasoning. Logic is a wide and ancient domain of study and intuitionistic logic is just a part and a quite recent one of it. You can find many interesting books about it. Let’s just remind that with respect to programming, intuitionistic logic can be observed in proof assistants & languages like Agda or Coq. I personally think those approaches are currently changing a lot the way we consider robust programming.
Closed Cartesian Categories… Those are much fuzzier in your everyday life. If you write some Haskell or use cats/scalaz in Scala, you already know Functors, Monoids, Monads, Applicatives etc… Those structures help a lot in representing/manipulating computations and operations on data in a safer way & then reflect sanely about your programs. Those structures come from Category Theory and Lambek established the link between typed 𝛌.calculus and closed cartesian categories in the 70s. Category Theory has been formalized by Lawvere in the 60s and since, has become very important to many domains of mathematics because it unifies a lot of concepts.
BTW, I recommend you to read and re-read P.Wadler’s Proposition as Types
Category theory can be a bit intimidating because it’s very abstract and it’s not always easy to accept the triviality of its purely intellectual constructions. This theory doesn’t care about the nature of things, it just cares about group of things, the rules defining those groups and the relations between those groups. Let’s quote Wikipedia definition even if there is no proof it’s true:
Category theory formalizes mathematical structure and its concepts in terms of a labeled directed graph called a category, whose nodes are called objects, and whose labelled directed edges are called arrows (or morphisms). A category has two basic properties: the ability to compose the arrows associatively and the existence of an identity arrow for each object.
Just remind 4 terms:
- morphisms (or arrows),
Now let’s scribble lines between Scala code, logic and category theory…
Type <> Object <> Proposition
In Scala, you’re manipulating simple Types which are groups/sets of values/elements :
- Int is the group of all integers (from -MAX_INTEGER to MAX_INTEGER), same for Doubles, Shorts, Floats etc…
- Boolean is a group of 2 values (True or False)
- Unit is a group of 1 value ()
A group of elements (finite or not) is called an Object in Categories. A category is simply a group/set of objects which are themselves groups/sets of elements… Categories just cares about the groups, not the elements themselves.
When you program in Scala (or any typed functional language), you might not be aware about it but you live in a golden categorical prison: you’re only concerned by a very specific category called category of sets, denoted as Set (yes it’s a confusing name). I’m simplifying a lot here (search “Hask category not a category”, you’ll find more) but let’s keep in mind that, in the typed programming scope, we only use Set. This category is a very well known one in which everything is much simpler to consider than in generic categories. Our life as developer is much easier in terms of categories than for a true mathematician.
In logic, any inhabited type (having at least one value) is equivalent to a “proposition” which can be interpreted into some truth value. Consequently, you can deduce that the uninhabited type
Nothing in Scala (
Void in Haskell) can be used to perform reasoning by contradiction or absurdity… “ex falso (sequitur) quodlibet” (Our latin ancestors weren’t so far from us ;))
Function <> Morphism <> Implication
In Scala, in most of your programming sessions, you write functions with an input of type A and an output of type B (and sooner or later you pass a value of type A to the function to compute things).
This simply establishes a relation between the group of values represented by type
A and the group of values represented by type
B. If you apply the function to any value from A, it will return a value from B (and same A always gives same B because your function should be referentially transparent or you’re not somebody I can trust).
A => B just represents the logic implication “if A then B”.
This relation in a Category between object
A and object
B is called a morphism and category theory is specially interested in those relations.
Objects & Types are related to themselves
In Scala, for every type, there is one single identity function which does nothing to its input but passing it to the output.
In a category, in the same way, every object has an identity morphism from itself to itself meaning every object is related to itself.
In logic, this just means any proposition implies itself which is tautologic.
Functions & Morphisms compose
In Scala, you all know that when you have a function from
A => B and another from
B => C then you can compose them to obtain a function from
A => C.
In category, all morphisms compose in the exact same way as functions and we’ll call this operator ○.
In logic, composition of propositions is just natural deduction:
If I know that A implies B and B implies C then I know that A implies C
Now, we have everything that defines a Category according to Wikipedia:
- objects <> types <> proposition
- morphisms <> function <> implication
- identity <> identity function <> self-implication
- morphism composition <> function composition <> natural deduction
Representing Category in Scala
Scala language, despite all its presumed defaults, allows to represent abstractions of “higher-order” beyond simple ones such as polymorphism. Thus, we can also write a Category in Scala language as a trait (equivalent to typeclass in Haskell):
- As said earlier, Scala Types are already objects in category Set so no need to care, we are already manipulating objects in a category.
- To be a category, a structure requires a morphism (or arrow)
->[A, B]so we parameterise the trait
Catby a higher-order type representing the morphism
->[A, B]from any object/type A to any other object/type B in the category.
- A category provides one identity morphism
idfor every object/type.
- A category provides the composition operation ○ between every morphism.
- For information, here are the other laws implied by category (identity & associativity composition).
In Scala, we live in category Set and if we take
Function1/=> as morphism plus the identity function plus the function composition, we can easily write a version of our
Cat trait for Scala
Take 2 seconds to think about the following.
id and ○ are written in Scala code but they belong to the language of categories, right?
Per CHL isomorphism, Scala simply-typed functions are equivalent to that language so it means we can rewrite such a basic Scala function into the language of Categories (within Scala).
This is nice but in the CHL isomorphism, it speaks about correspondence to Closed Cartesian Categories, not just Categories.
Yes that’s right because you need a few more concepts to write meaningful functional programs.
Cartesian product or logical conjunction
When you solve problems, your mind often thinks in the following way:
If I know A implies B and A implies C then I know A implies (B and C)
I also know that (A and B) implies A and also B
A and B is often written using boolean logic operators
A ^ B.
𝛌.calculus is very basic and is often augmented with Cartesian Product of 2 types
A x B to simplify syntax.
In a program, the usefulness of cartesian product seems obvious:
- it allows to build more complex types such as case classes (or records in Haskell) and use projections to extract data from them.
- it allows to “aggregate” 2 functions with the same input type and different output type into one single function.
In terms of category, this definition of Cartesian Product with the 2 projections correspond exactly to the definition of Cartesian Category. Surprising, isn’t it?
So let’s do the same exercise as above and enhance our
Cat trait into a
CartesianCat trait defining the requirements of our Cartesian Category.
- ⨂ is just the expression of above conjunction replacing implication by morphism.
(C, D)is written using Scala Tuple but keep in mind that it’s the product in the Cartesian Category.
exrare just the 2 projection operations.
So our category language have been augmented with 3 more operations ⨂, exl, exr
The same can be written about the dual of Product called Coproduct or Disjunction in logic
A ∨ B (A or B). You can then build a Cocartesian Category but I won’t write it here, it’s trivial.
If you mix both Cartesian and Cocartesian categories into one single, you obtain the so-called Bicartesian Category.
Apply a function aka Modus Ponens
When you write a function
A => B , you naturally expect to apply it on some value
A to obtain a value
B(and again, same A shall always return same B…)
In terms of category, for any object/type
B, it means we have a unique function
(A => B, A) => B. This is called “applying function to value” (or evaluating).
That sounds very trivial, right? But, this is one of the most basic rule of logic called modus ponens.
If you know A implies B and you prove me A then I can prove B
So, applying a function on a value is just applying the modus ponens.
Just for the story,
(A => B, A) => B is not exact, it should be
(A ^^ B, A) => B with
^^ meaning exponential. In our Category Set, the exponential is synonym to
=> but in other categories, exponential can be something else. You can read more about categorical exponentials in Bartosz Milewski’s post https://bartoszmilewski.com/2015/03/13/function-types/ and you’ll see how “ exponential” name in category was chosen because it behaves like numerical exponentials and shows why category theory has become important: it unifies things.
A terminal object for empty products
In general, we want to manipulate products of any arity, from 0 (empty product) to infinity (Actually historically till the famous biblic limit of 22 in Scala).
The empty product is a product of 0 object and is a unique value
(). The type of this value is a type being inhabited by the single value
() and you know one such type in Scala:
Moreover, for any object/type
A, you can easily build a simple function/morphism:
A => () = (a:A) => ()
Having this property in a category means
() is a terminal object in the category and the empty product is also the terminal object itself.
With product defined above and this terminal object, it’s easy to generalise products & projections: the product of
n elements being the product of the
n-th element and a product of
n-1 elements, recursively till 0.
Currification / Uncurrification
In 𝛌.calculus, there is no function with multiple parameters like in Scala. A function with 2 parameters becomes a function with 1 parameter that returns a function with 1 parameter. This is called currying a function and Haskell only manages curried functions.
In terms of category, it means we have the following morphism :
((A, B) -> C) -> (A -> B -> C)
The dual of that is called uncurrying:
(A -> B -> C) -> ((A, B) -> C)
So any function with multiple parameters can be transformed into a succession of functions with one parameter and vice-versa.
No need to discuss more about currying/uncurrying, it’s really a basic feature of functional programming. It also allows manipulating only functions with 1 parameter and this can simplify a lot of considerations and manipulations.
… Finally Closed Cartesian Category…
In the context of cartesian category, if we add the 3 previous operations:
- function apply,
- terminal object,
… we finally obtain everything required by a Closed Cartesian Category…
Let’s augment our CartesianCat with those new operations:
… And again, we can write
Now, we have a full set of operations written in Scala but belonging to the language of Closed Cartesian Categories parameterised by the type of morphism in this CCC.
According to Curry-Howard-Lambek isomorphism, we can rewrite every piece of Scala code (restricted to simply typed lambda) into that CCC language and vice-versa.
Part2 — Compiling primitive function to CCC in Scala
Now, you know what is a Closed Cartesian Category and why there is an isomorphism between it and simply-typed lambda and logic.
Then, let’s focus on the original idea of compiling primitive Scala function to CCC language.
Rewriting Scala code into CCC
The best is to see a very simple example. Let’s write it manually to get the idea.
That’s amazing, right?
You had a very simple & short function, it has become something much longer and very strange, what a success! But but but, it is written in the language of CCC!
Actually, it’s not exact as
+ function is not a CCC operation but a Scala function on primitive typed value (such as Int, Double, Float, Short, etc…). Thus, we need to augment our CCC by adding support for such primitive-types operations.
… And finally we can use that CCCNumExt in our previous rewrite.
Now we are fully in CCC language…
if you call
plus(14, 28) on both equivalent lines, I promise, you will obtain
You suffered a lot to reach this point of the post and you certainly wonder why so many efforts to rewrite a nice little Scala function into something much less usable.
The response is…
CartesianClosedCat[Function1]is one CCC but there are many other Cartesian Closed Categories around, having the same internal language but interpreting totally differently.
So, once you can rewrite your Scala code into the CCC language, you can then interpret it with any CCC.
Graphs of computation can be CCC
I haven’t invented anything here and I just copy Conal Elliott because it‘s cool enough like that.
Forget logic and just believe the following: it is possible to represent directed graphs in a kleisli-like structure accepting the input ports and returning a State monad that supplies the output ports and a list of instantiated components along the directed graph construction.
Here is the definition of this Kleisli-State-monadic-like directed Graph in Scala.
You certainly concluded that this
Graph[A, B] structure forms a nice Closed Cartesian Category using
Graph as a morphism.
So we can implement our
Finally, let’s switch previous rewrite from
Function1 CCC to
If you run the
plus function in the
Graph CCC, you obtain a directed graph of your computation and you can translate it again into a nice graphviz representation for example.
Got the idea, now?
If you can build a computation graph because it’s a CCC, you can translate it in anything that is compliant to CCC language augmented with the right extensions (numerics, booleans etc…). So, you could imagine compiling into a specific hardware language for example (as Conal explains in his paper). He also evokes translations of linear functions into data (matrices) or transforming functions into their automatic differentiated forms. I might explore that thing one day because it’s really cool…
One last interesting fact: the product of 2 CCC is a CCC so you can compile your Scala code once in CCC language and then run it into 2 different CCCs at the same time… Great :D
Scalafix to the rewriting rescue?
The last but not the least:
How can we rewrite Scala code automatically into CCC language?
Conal Elliott in his paper works in Haskell and in Haskell you can write a compiler plugin and use rewrite rules.
Scalameta allows to represent Scala code into a simple and clear Meta AST that you can manipulate quite easily. Scalafix allows to develop rules that introspects your Scala code translated into ScalaMeta AST and pattern-matches directly on pieces of code using the so-called wonderful quasiquotes. Then you can patch easily this piece of code and rewrite the original code. Scalafix allows automatising most of your lib/API migrations for example.
To perform my Scala to CCC rewrite, I decided to try using a Scalafix rule.
I won’t show my current code right now because it’s experimental and ugly and not generic at all. But the idea is the following:
The rest is just experimental tooling and trust me, it can work all together ;)
We have digressed a lot around Curry-Howard-Lambek isomorphism, the simply-typed 𝛌.calculus, intuitionistic logic and category theory. But I felt it would be useful (at least for me).
We have shown that we could rewrite some Scala code (with a few restrictions) into the Closed Cartesian Category language using a Scalafix rule. We can also interpret the rewritten code into a different destination Closed Cartesian Category than Set/=> and this is really promising.
I don’t pretend this is a viable solution for now and even a good solution to compile languages into others as you need to restrict your domain to typed lambda and write custom extensions for numerics and more. But, the study is really worth IMHO.
I also think it’s a very nice playground to become aware about the bridges drawn between your programs & types, your domain logic and the formalisation of the underlying rules, links and laws your computations imply.
Harper wrote about “computational trinitarianism”:
The central dogma of computational trinitarianism holds that Logic, Languages, and Categories are but three manifestations of one divine notion of computation. There is no preferred route to enlightenment: each aspect provides insights that comprise the experience of computation in our lives.
These ideas are amazing to me and really opened my mind to new horizons. At 41, I don’t doubt much anymore that I can find a reasonable solution to a problem. But now, the route I take is much more important than reaching the destination itself.
Driving on highways pleases your bosses in general but it rarely leads you to enlightenment. Finding your own “route to enlightenment” is something terribly important, very personal and that our professional business tends to bury or even deny.
Yet, I’ve remarked that smaller winding roads often lead to amazing unexpected places. There, I often meet great people sharing the same ideals as me. We discover together, learn and enjoy. Then, serendipity lets me discover a hidden space capsule that leads me directly to the destination in a rocket flight to enlightenment! And oddly, I feel like a better developer and person…