This post assumes some familiarity with type level programming in Scala, specifically I use a bit of Shapeless.
It also requires some understanding of the fixpoint type
Fix. If you want to learn about it, the following resources have been helpful to me:
- Pure Functional Database Programming with Fixpoint Types by Rob Norris at Scala World 2016
- The Y Combinator (Slight Return) by mvanier.
- Understanding F-Algebras by Bartosz Milewski
- Datatype generic programming in Scala - Fixing on Cata by Debasish Ghosh.
- Matryoshka's README.
What is this about ?
The basic idea is actually pretty simple. Given that you can abstract away recursion in a type definition using
Fix, is it possible to create type that abstracts typelevel recursion.
Put simply, if I can use
Fix to implement a
List, is there something (
HFix ?) that I can use to implement
HList without explicitly having to deal with typelevel recursion? Even more challenging, can we do that in Scala?
SPOILER ALERT: The answer is YES. And it ends up being (almost) as simple as
Fix again ?
Ok so just to make sure I understood the everything I've read, I started by reimplementing
Fix. This is of course a trivial job, as it just fit in one line:
That's great, but it does not tell me how to implement a
List. So I went on and implemented a
List[A]. Most of the articles I've read fix the
A and implement a
IntList. Since I like bit of challenge and wanted to be sure I understood everything, I went to the slightly harder path of implementing a trully generic
A list element is either
Nil. Apart for some fiddling with the types and the absence of recursion, this should be pretty easy to understand:
Now that I have the basic pieces, the only thing left to do is to actually build a
List. Let's define a couple of constructors, and a type alias to make things nicers:
And now we can build a
How do I implement the same thing at the type level ?
I must admit it took me a bit of time to come up with the following piece of code. I'm quite satisfied with it thought.
It also took me some time to really get
Fix at first. I guess it's one of those ideas that are really simple, but somehow hard to get until the "AHA!" moment. Writing this was in the same vein. A lot of struggling, and "AHA!" it's actually really simple (then I felt bad for having struggled so much on this...).
Here's the code (Yeah I know, I'm terrible at naming things. Any help appreciated):
So just like in the definition of
Fix, this type is recursive. There's 2 little tricks to understand:
*, we have recursion at the type level. So contrarily to
Fix, not every element in the recursion have the same type.
- I added a
INiltype. At some point we'll need to stop the recursion. This type will have no inhabitant, and just serves that purpose.
Creating an HList
Now how does this help me implementing
HList ? Well, there it becomes really cool. You see, the only difference between a
List and a
HList is the recursion scheme. A
HList is recursive at both the type and value level at the same time, while a
List is only recursive at the value level. Apart from that, they are the same. Therefore, I can reuse the previously defined
Cons, and I just have to provide new constructors:
Again, I added type aliases, they're really not necessary, as
Scalac infers types perfectly, but I think they help the reader.
hnil is particularly interesting. The empty
Nil and the end of type level recursion denoted by
Now can I build HLists ?
Just as easy as a normal
C'est le caca, c'est le cata, c'est le catamorphisme!
(Sorry this joke does not translate).
So far we've defined ways of building
HList in terms of
From there it seems only natural to try to implement a catamorphism.
Fix it's pretty straightforward:
Of course we need a functor for
F. Since we're going to test this with our newly defined
List, I'm going to define it immediately for
Now let's try something simple:
Now let's try to implement a catamorphism for
HFix. This one is slightly more involved. I'm going to need polymorphic functions here. Luckily Shapeless provide those:
Interestingly, you also only need a functor for
F. Now let's try this:
And again in works !
The last thing I wanted to try was to implement
Coproduct in terms of
Now the constructor for
Coproduct is a bit more complex that
List. We need to be able to
Inject values into our
Coproduct. Let's implement that. It is very similar to Shapeless':
A simple test again:
Yep. it works :).
All this raised a lot of other questions:
- Can this be used to actually build something useful ?
- What about corecursive types ? Do they exist ? Can we implement an anamorphism ?
- Can we define "infinite" types (like a Stream of types)? Would it make sense ? This would probably require lazyness at the type level.
- Could we implement a Y-combinator in the type system ?
I guess I'm just going to continue playing around with this for a while. Any new idea or feedback is appreciated, either in the comments or on twitter.