GADTs and Superpositions in Raku
In my last post, I talked about this bit of code for implementing a Maybe ADT in Raku:
role Maybe[::A] { }
sub just(::A $x --> Maybe[::A]) { class Just does Maybe[::A] { has $.V = $x; }.new }
sub nothing(Any:U $t --> Maybe[$t]) { class Nothing does Maybe[$t] { }.new }
I knew this code was bad but at the time I couldn’t figure out how to improve upon it. Rest easy, though, as Raku has us covered. Enter the junction….
A junction is a special type that represents a superposition of eigenstates that collapse down to a single value in a boolean context. In English, it’s a type that is hand-crafted to match against values in special ways. Consider this simple conditional:
if 2 + 2 == 4 or 2 + 2 == 6 {
say 'raku can do math!'
}
(Obviously 2 + 2 will never equal anything but 4, but in the case of some sort of reality bending apocalyptic event, we can never be too sure.)
This conditional can be rewritten using a junction as:
if 2 + 2 == 4|6 {
say 'raku can do math /and/ collapse superpositions!'
}
In this case, the == operator autothreads over the junction, effectively mapping each value to whether or not it equals 2 + 2. We can see this by looking at this session:
trepl> 4|6 # This is simply the junction of values `4` and `6`.
==> any(4, 6)
trepl> 2 + 2 == 4|6 # This is autothreading over `4|6` using `==`.
==> any(True, False)
trepl> ?(2 + 2 == 4|6) # This is coercing that result to a boolean.
==> True
So, what does this have to do with GADTs? Or, perhaps more importantly…
What is a GADT? #
(tl;dr: https://en.wikibooks.org/wiki/Haskell/GADT)
GADT stands for “Generalized Algebraic Data Type”, and it’s essentially a highly generalized way to represent the constructors of a given type.
Consider the following Haskell snippet defining an extremely simple data type: OurNullable This type will work exactly the same as, say, Nullable<T> from Java – thus managing to anger both Haskell programmers and Java programmers simultaneously. Our type can be constructed by either calling OurNull with no arguments or OurFull with one argument. It looks like this in Haskell: (do note that this is automorphic to the Maybe type)
data OurNullable t = OurNull | OurFull t
But, what if we wanted to impose some arbitrary constraint onto the type we put in OurNullable? That’s where GADTs come in. Let’s say that instead, we only want values that we can call == on inside OurNullable. We would modify the OurFull constructor to only take in values which have this property. That looks like this:
{-# LANGUAGE GADTs #-}
data OurEqNullable t where
OurNull :: OurEqNullable t
OurFull :: Eq t => t -> OurEqNullable t
Do note that we can also write the original version of OurNullable as a GADT as well:
{-# LANGUAGE GADTs #-}
data OurNullable t where
OurNull :: OurNullable t
OurFull :: t -> OurNullable t
That’s all you’ll need to know about GADTs in order to appreciate the Raku heading your way.
Putting it all together #
Alternatively, collapsing the eigenstates #
Now we’re ready to represent Maybe[::T] as a GADT instead of a hacky role as we did at the top. For clarity’s sake, we’ll discard with this notion of Maybe and instead redefine OurNullable. Let me show you the whole thing before we break it down into pieces.
# Helper function
sub prefix:«>»($x) { $x.v; }
# Constructor 1
class OurNull { has $.t is required;
method ACCEPTS($other) { $other.WHAT eqv OurNull and $other.t ~~ $!t } }
sub ourNull(Any:U $t) { OurNull.new: t => $t }
# Constructor 2
class OurFull { has $.v is required;
method ACCEPTS($other) {
$other.WHAT eqv OurFull and do {
with $!v { >$other ~~ $!v.WHAT }
else { >$other ~~ $!v } } } }
sub ourFull($v) { OurFull.new: v => $v }
# Data declaration
sub IsNullable(Any:U $t) { ourNull($t) ^ ourFull($t) }
# Usage:
my $fill-it-up where IsNullable(Str) = ourFull('Raku rocks!');
my @possibly-list where IsNullable(Int) = ourNull(Int), ourFull(3), ourFull(5);
proto print-our-nullable($ where IsNullable(Any)) {*}
multi print-our-nullable(OurFull $m) { (>$m).say }
multi print-our-nullable(OurNull $) { 'null'.say }
@possibly-list.map: &print-our-nullable;
First, we define a helper function prefix:«>»($x) at the top of the file. This isn’t necessary per se, or even really necessary, but in my opinion it’s nicer to have dedicated syntax for unwrapping values like this.
Constructor 1: OurNull #
class OurNull { has $.t is required;
method ACCEPTS($other) { $other.WHAT eqv OurNull and $other.t ~~ $!t } }
sub ourNull(Any:U $t) { OurNull.new: t => $t }
This is the first constructor in our GADT, equivalent to the OurNull :: OurNullable t line in our Haskell implementation. We separate the type with its constructor by capitalization, so OurNull is the type which we construct using the routine ourNull.
The ACCEPTS function is used during typechecking – we only succeed in typechecking if we match against another instance of OurNull and if the type that’s contained within OurNull matches against the type passed in.
Constructor 2: OurFull #
# Constructor 2
class OurFull { has $.v is required;
method ACCEPTS($other) {
$other.WHAT eqv OurFull and do {
with $!v { >$other ~~ $!v.WHAT }
else { >$other ~~ $!v } } } }
sub ourFull($v) { OurFull.new: v => $v }
Most of what is here is the same as before, with the exception of the ACCEPTS method. This time, we must have two branches related to the two scenarios which may end up calling ACCEPTS: when OurFull contains a type vs. when OurFull contains a value.
We use “undefined” instances of OurFull (ones that contain types instead of values) in the next section. In normal usage, most users will end up running into the latter case >$other ~~ $!v, in which case it returns the smartmatch of an unwrapped OurFull against an unwrapped version of itself.
The GADT Junction #
# Data declaration
sub IsNullable(Any:U $t) { ourNull($t) ^ ourFull($t) }
Here’s where all the magic happens!
Finally, we’ve reached the data OurNullable t where... line. The reason I didn’t call this routine OurNullable is because there’s a fundamental difference in how we use this method versus how we’d use a normal type. IsNullable actually returns a junction of OurNull and OurFull instances.
When matching against this junction, the superpositions collapse into a truthy value (the match succeeds) if one and only one of the superpositions match, according to the ACCEPTS method. The superpositions collapse into a falsy value (the match fails) if any other case occurs.
So, this junction doesn’t represent an actual type, it represents something we’re going to match types against. Thus we must use a where block, which allows us to only accept a certain type if the type matches with a given predicate.
Usage #
my $fill-it-up where IsNullable(Str) = ourFull('Raku rocks!');
my @possibly-list where IsNullable(Int) = ourNull(Int), ourFull(3), ourFull(5);
proto print-our-nullable($ where IsNullable(Any)) {*}
multi print-our-nullable(OurFull $m) { (>$m).say }
multi print-our-nullable(OurNull $) { 'null'.say }
@possibly-list.map: &print-our-nullable;
The usage of IsNullable ends up being very similar to the usage of Maybe[::T]. The only caveat is that the where clause forces the typechecking of IsNullable types into runtime. This incurs a non-negligible overhead. For more on this, check out the previous article Raku is the World’s Worst ML.
Drawbacks #
This method of handling GADTs is slow. For every runtime type check that occurs, &IsNullable must create an entire class for every constructor in the GADT. For this tiny little example, that’s fine, but for an entire application it would become problematic.
After looking back at this implementation vs. the original one we’ve started with, I’m actually very disappointed at how this turned out. I thought that using junctions would simplify things – but it merely ended up moving type checking to runtime. On the bright side, this movement of type checking to runtime means that we can further constrain the types we want to allow in our Nullable by constraining the type of IsNullable, but it’s a small benefit for a huge cost. The only real improvement that we’ve made over the original implementation is the introduction of the unwrapping operator prefix:«>»($x), which is not specific to this implementation at all.
Nonetheless, there’s enough valuable information here that I’m still excited to share it with you all. It’s a really unique and flexible way of looking at problems – one that’s highly inspired by the functional, data-oriented paradigm.
Special thanks to guifa and AlexDaniel in the IRC (#perl6 on freenode) for talking through this a little bit with me.
