This algorithm completely hides the implementation details of Backend and ternary.
Sum.
Aux and all the rest from the user, the same way Int’s version of + hides the implementation from the user.
It’s completely generic.
Let’s take it for a spin:The first example uses TNat under the hood, and the second example uses BNat under the hood.
I cannot stress enough just how cool this is — the end user has no idea the compile-time machinery that is turning behind the scenes.
AlgorithmsOf course, now we can apply one operation why shouldn’t we do several things at once?Consider the following typelevel function:What we want to do is take the GCD of two symbols, add 7 to it, and square the result.
By now the implementation should be easy for you to imagine:The implicit algorithm there literally just says “Take gcd, add 7, square it”.
All completely free of any knowledge of any implementations used.
Here’s an example of it working:In fact, each step uses a different backend: mult uses BNat, sum uses TNat and gcd uses shapeless.
Nat.
There’s one small thing I want to really press home here: At no point in the implementation of Symbol did I write a GCD algorithm.
In fact, I’ve never even read shapeless’ implementation of GCD.
And yet here, we’re free to use it randomly in the middle of an unrelated concept, apparently nothing to do with shapeless.
Nat in the slightest.
The mere act of adding in some implicit SymbolMappings for shapeless has allowed us to lift all of shapeless.
Nat functionality to Symbol and interoperability with BNat and TNat and others, without ever having to read or understand the implementations.
All we have to do is a few symbol mappings, and trust shapeless devs know what they’re doing when they write a typelevel GCD algorithm.
One final bit of coolnessAs I’ve said many times by now, the algorithms we’re writing are completely free of any knowledge of the backend and algorithm used.
Imagine running GcdPlus7Squared on some input.
Here’s an example, just like above:Now, that goes to shapeless.
Nat, TNat and then finally BNat.
But… Recall how we mapped operations to algorithms in the first place:Let’s just make a tiny change and point this at TNat’s multiplication algorithm instead:Now let’s run our toy function again:Obviously the result is the same: We didn’t change arithmetic (and it goes to show that our BNat and TNat algorithms are consistent with each other).
But that tiny change above, from BNat to TNat, has vastly changed the hidden machinery behind our symbols.
The compiler now uses TNat for multiplication!.A completely different algorithm with a different efficiency profile and different strengths and weaknesses, a completely different path for the compiler with different types and different recursion, changed by altering two small words.
Our public code, the function GCDPLus7Squared, is entirely unchanged.
Pull a tiny lever and the whole world turns, and the end user has no idea you did anything at all³.
The above code and concepts are available for you to play around with in the TypeChecked project Symbology.
Symbology contains an example which demonstrates vast efficiency improvements when silently swapping between shapeless and TNat algorithms behind the scenes.
Due to the limitation of using a milestone version of Scala, this is sadly unusable in normal day-to-day code.
But hopefully it demonstrates the power typelevel programming can have, and may act as inspiration for more typelevel libraries in future scala versions.
[1] Our new language-at-compile-time we’re building, with our own syntax for function application and everything, isn’t actually statically typed.
This is because it’s not compiled.
The jvm compile-time is our run-time.
This new language has no corresponding compile-time.
A ‘type-error’ in this language results in an end to the scalac compilation, which is the equivalent of an exception during our run-time.
[2] These implicits must be def.
If you make them vals, everything stops working.
I genuinely have no idea why, maybe someone smarter than me can tell me.
I was very lucky that the first time I wrote this I wrote them as defs on reflex, before later tightening to vals and having everything break on me.
If I’d written them as vals first I likely would have assumed the whole concept of this post was impossible.
[3] Apart from potential efficiency gains and losses.
If we had instead written a TNat GCD algorithm, and swapped that in instead of using shapeless’, then our toy function would see a huge efficiency upgrade without the end user having to do a single thing.
The difference between BNat and TNat multiplication at this magnitude of calculation is not large enough to see a difference in compile times.
Thanks to Jack Wheatley for the help.
.. More details