# Compiling Scala into Closed Cartesian Categories language using ScalaFix rewriter

The idea in this post is to experiment with 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 & especially 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.

*Disclaimer*

*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 drawbridges 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 a 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 theory1 formalizes mathematical structure and its concepts in terms of a labelled 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 remember 4 terms:

*objects**morphisms (or arrows)**identity**composition*

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 care about the groups, not the elements themselves.

When you program in Scala (or any typed functional language), you might not be aware of 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 a 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 as 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).

```
f: A => B = { (a:A) => e // e do something with a }
// written in 𝛌-calculus style
// 𝛌(a:A). e with (e:B)
```

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 the same B because your function should be referentially transparent or you’re not somebody I can trust).

In logic, `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 especially 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.

```
id: A => A = identity
// 𝛌(a:A). a
```

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`

.

```
f: A => B = ???
def g: B => C = ???
def h: A => C = g compose f
```

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 representing 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):

```
Cat[->[_, _]] {
def id[A]: A -> A
def ○[A, B, C]: (B -> C) => (A -> B) => (A -> C)
}
```

- 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`Cat`

by 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
`id`

for 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 the context of a Category def f: A => B = ??? // ≌ representing isomorphism f ○ Id ≌ Id ○ f ≌ f // associativity (h ○ g) ○ f ≌ h ○ (g ○ f)`

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 `Function1[A, B]/=>`

.

```
val Function1Cat: Cat[Function1] = new Cat[Function1] {
def id[A]: A => A = identity
def ○[A, B, C]: (B => C) => (A => B) => (A => C) = f => g => f compose g
}
```

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

For example:

```
simple identity function
def f: A => A = identity
// if I have an implicit Cat[=>] in my scope
val K = implicitly[Cat[Function1]]
// I can rewrite f into the language of categories
def f = K.id[A]
// Both are equivalent by the CHL isomorphism...
```

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.

```
lambda calculus augmented with cartesian product (A x B) and 2 projections from (A x B) to A and B
// projection1 from (A x B) to A
𝚷1(a:A, b:B) = a:A
// projection1 from (A x B) to B
𝚷2(a:A, b:B) = b:B
// cartesian product expressed in terms of the 2 projections
(𝚷1(c:A ⨂ B), 𝚷2(c: A ⨂ B)) = (c: A ⨂ B)
```

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.

```
CartesianCat[->[_, _]] extends Cat[->] {
def ⨂[A, C, D]: (A -> C) => (A -> D) => (A -> (C, D))
def exl[A, B]: (A, B) -> A
def exr[A, B]: (A, B) -> B
}
```

- ⨂ 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.`exl`

and`exr`

are 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 `A`

and `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: `Unit`

.

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 opposite 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
- currying/uncurrying

We finally obtain everything required by a Closed Cartesian Category

Let’s augment our CartesianCat with those new operations:

```
ClosedCartesianCat[->[_, _]] extends CartesianCat[->] {
def it[A]: A -> Unit
def ap[A, B]: ((A -> B), A) -> B
def curry[A, B, C]: ((A, B) -> C) => (A -> (B :=> C))
def uncurry[A, B, C]: (A -> (B -> C)) => ((A, B) -> C)
}
```

And again, we can write `ClosedCartesianCat[Function1]`

.

```
val Function1ClosedCartesianCat: ClosedCartesianCat[Function1] = new ClosedCartesianCat[Function1] {
def id[A]: A => A = identity
def ○[A, B, C]: (B => C) => (A => B) => (A => C) = f => g => f compose g
def ⨂[A, C, D]: (A => C) => (A => D) => (A => (C, D)) = f => g => (a => (f(a), g(a)))
def exl[A, B]: ((A, B)) => A = _._1
def exr[A, B]: ((A, B)) => B = _._2
def it[A]: A => Unit = _ => ()
def ap[A, B]: ((A => B, A)) => B = f => f._1(f._2)
def curry[A, B, C]: (((A, B)) => C) => (A => (B => C)) = f => a => (b => f((a, b)))
def uncurry[A, B, C]: (A => (B => C)) => (((A, B)) => C) = f => { case (a, b) => f(a)(b) }
}
```

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.

```
a very basic Scala function performing a simple operation on primitive type Int
def plus = (x:Int) => (y:Int) => x + y
// First, we need to reify our CCC world
val K = implicitly[CartesianClosedCat[Function1]]
// now we import CCC language into our context
import K._
// pseudo-code
// we can always uncurry curried function
uncurry((x:Int) => (y:Int) => x + y) ≌ (x:Int, y:Int) => x + y
// remind projections
(x:Int, y:Int) => x ≌ exl[Int, Int]
(x:Int, y:Int) => y ≌ exr[Int, Int]
// now use product
{ (x:Int, y:Int) => x } ⨂ { (x:Int, y:Int) => y } ≌ (x:Int, y:Int) => (x, y)
// using projections it can be rewritten
exl[Int, Int] ⨂ exr[Int, Int] ≌ (x:Int, y:Int) => (x, y)
// now compose with + : (Int, Int) => Int
( + ) ○ { (x:Int, y:Int) => (x, y) } ≌ x + y
// or
plus ≌ ( + ) ○ (exl[Int, Int] ⨂ exr[Int, Int])
```

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.

```
We can write this type class parameterized by the morphism and a type A
trait CCCNumExt[->[_, _], A] {
def negateC: A -> A
def addC: (A, A) -> A
def mulC: (A, A) -> A
}
// and implement it for Function1 and any Numeric A
implicit def Function1CCCNumExt[A](implicit N: Numeric[A]): CCCNumExt[Function1, A] = new CCCNumExt[Function1, A] {
def negateC: A => A = N.negate _
def addC: ((A, A)) => A = { case (a, b) => N.plus(a, b) }
def mulC: ((A, A)) => A = { case (a, b) => N.times(a, b) }
}
// just note the trick: we put A in the trait type parameters
// to be able to constrain it later with Numeric
```

And finally we can use that CCCNumExt in our previous rewrite.

```
plus = (x:Int) => (y:Int) => x + y
// First, we need to reify our CCC language
val K = implicitly[CartesianClosedCat[Function1]]
// First, we need to reify our CCC numeric extensions for Int (ok it's a bit hard coded but that's not the point here ;))
val E = implicitly[CCCNumExt[Function1, Int]]
// now we import CCC language into our context
import K._, E._
// the line on top is strictly equivalent to the following in CCC language
def plus = addC ○ (exl[Int, Int] ⨂ exr[Int, Int])
```

Now we are fully in CCC language…

If you call `plus(14, 28)`

on both equivalent lines, I promise, you will obtain `42`

.

### But why????

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:

```
A port is just identified by an Int
type Port = Int
// A component has a name and input/ouput ports
final case class Comp[A, B](name: String, inputs: Ports[A], outputs: Ports[B])
// the state monad building the list of components Comp
type GraphM[A] = ((Port, List[Comp[_, _]])) => ((Port, List[Comp[_, _]]), A)
// the kleisli-like directed graph structure based on state monoad
final case class Graph[A, B](f: Ports[A] => GraphM[Ports[B]])
// For info, the different type of ports
sealed trait Ports[A]
case object UnitP extends Ports[Unit]
final case class BooleanP(port: Port) extends Ports[Boolean]
final case class IntP(port: Port) extends Ports[Int]
final case class DoubleP(port: Port) extends Ports[Double]
final case class PairP[A, B](l: Ports[A], r: Ports[B]) extends Ports[(A, B)]
final case class FunP[A, B](f: Graph[A, B]) extends Ports[A :=> B]
```

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 `ClosedCartesianCat[Graph]`

.

```
our CCC with Graph as morphism
implicit val GraphCCC: ClosedCartesianCat[Graph] = new ClosedCartesianCat[Graph] {
// long boring useless code
}
// we can also implement CCCNumExt for Graph
implicit def GraphCCCNumExt[A](implicit N: Numeric[A], gp: GenPorts[A]): CCCNumExt[Graph, A] = new CCCNumExt[Graph, A] {
// genComp just generate a component with 2 inputs, 1 output and a nice name
def negateC: Graph[A, A] = genComp("-")
def addC: Graph[(A, A), A] = genComp("+")
def mulC: Graph[(A, A), A] = genComp("*")
}
```

Finally, let’s switch previous rewrite fromFunction1 CCC to `Graph`

CCC.

```
plus = (x:Int) => (y:Int) => x + y
// First, we need to reify our CCC language
val K = implicitly[CartesianClosedCat[Graph]]
// First, we need to reify our CCC numeric extensions for Int (ok it's a bit hard coded but that's not the point here ;))
val E = implicitly[CCCNumExt[Graph, Int]]
// now we import CCC language into our context
import K._, E._
// the line on top is strictly equivalent to the following in CCC language
def plus = addC ○ (exl[Int, Int] ⨂ exr[Int, Int])
```

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.

```
You can run the plus function rewritten in Graph CCC
// and it will build a nice directed graph of your computation
val dGraph = Graph.runGraph(plus)(14, 28)
// now you can translate that directed graph into a nice format like graphviz
Graph.toGraphViz("plus")(dGraph)
```

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?

Last but not 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.

In Scala, since a few months, we have a wonderful toolbox: Scalafix + Scalameta.

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:

```
Fake Scalafix rule to rewrite Scala to CCC
// Just so that you catch the idea
final case class CCCRule(index: SemanticdbIndex) extends SemanticRule(index, "CCCRule") {
def convertSubTree(ctx: RuleCtx, v: Tree, tree: Tree): Tree = {
tree match {
// the identity morphism
case t@q"$x => ${y: Term.Name}" if (x.name.isEqual(y)) =>
q"""K.id[${x.decltpe.get}]"""
// the plus function completely hardcoded and supposing we have CCC & CCCNumExt in the context
case t@q"$px => $py => $x + $y" =>
q"""○(addC)(⨂(exl[${x.decltpe.get}, ${x.decltpe.get}])(exr[${px.decltpe.get}, ${py.decltpe.get}]))"""
}
override def fix(ctx: RuleCtx): Patch = {
val trees = convertTree(ctx, ctx.tree)
trees.map { case (tree, newTree) => ctx.replaceTree(tree, newTree.toString) }.asPatch
}
}
```

The rest is just experimental tooling and trust me, it can work all together ;)

### Conclusion

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 noticed 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…

Originally published on medium.com