Ayaz Hafiz
It has never been enough to resolve a specialization lambda set by simply pulling down the specialized type of the lambda set into the target context, because specialized lambda sets can themselves be polymorphic. To correctly resolve such polymorphic specializations, I propose resolving lambda sets by unifying their ambient arrow types in a “bottom-up” fashion.
This is not an academic exercise. It comes up often in real programs. It’s unfortunately a blocker for interesting usages of abilities, like in our encoders/decoders.
In this section I’ll explain how lambda sets and specialization lambda sets work today, mostly from the ground-up. I’ll gloss over a few details and assume an understanding of type unification. The background will leave us with a direct presentation of the current specialization lambda set unification algorithm, and its limitation.
Lambda sets are a technique Roc uses for static dispatch of closures. For example,
id1 = \\x -> x
id2 = \\x -> x
f = if True then id1 else id2
has the elaboration (solved-type annotations)
id1 = \\x -> x
^^^ id1 : a -[[id1]] -> a
id2 = \\x -> x
^^^ id2 : a -[[id2]] -> a
f = if True then id1 else id2
^ f : a -[[id1, id2]] -> a
The syntax -[[id1]]-> can be read as “a function that dispatches to id1". Then the arrow -[[id1, id2]]-> then is “a function that dispatches to id1, or id2". The tag union [id1, id2] can contain payloads to represent the captures of id1 and id2; however, the implications of that are out of scope for this discussion, see Folkert’s great explanation for more information. During compile-time, Roc would attach a run-time examinable tag to the value in each branch of the f expression body, representing whether to dispatch to id1 or id2. Whenever f is dispatched, that tag is examined to determine exactly which function should be dispatched to. This is “defunctionalization”.
In the presence of abilities, lambda sets get more complicated. Now, I can write something like
Hash has hash : a -> U64 | a has Hash
zeroHash = \\_ -> 0
f = if True then hash else zeroHash
The elaboration of f as f : a -[[hash, zeroHash]]-> U64 is incorrect, in the sense that it is incomplete - hash is not an actual definition, and we don’t know exactly what specialization of hash to dispatch to until the type variable a is resolved. This elaboration does not communicate to the code generator that the value of hash is actually polymorphic over a.
To support polymorphic values in lambda sets, we use something we call “specialization lambda sets”. In this technique, the lambda under the only arrow in hash is parameterized on (1) the type variable the hash specialization depends on, and (2) the “region” in the type signature of the specialization that the actual type should be recovered from.
That was a lot of words, so let me give you an example. To better illustrate how the mechanism works, let’s suppose Hash is actually defined as Hash has hashThunk : a -> ({} -> U64) | a has Hash. Now let’s consider the following program elaboration:
Hash has
hashThunk : a -> ({} -> U64) | a has Hash
# ^^^^^^^^^ a -[[] + a:hashThunk:1]-> ({} -[[] + a:hashThunk:2]-> U64)
zeroHash = \\_ -> \\{} -> 0
#^^^^^^^ a -[[zeroHash]]-> \\{} -[[lam1]]-> U64
f = if True then hash else zeroHash
#^ a -[[zeroHash] + a:hashThunk:1]-> ({} -[[lam1] + a:hashThunk:2]-> U64)
The grammar of a lambda set is now
lambda_set: [[(concrete_lambda)*] (+ specialization_lambda)*]
concrete_lambda: lambda_name ( capture_type)*
specialization_lambda: <type>:ability_member_name:region
region: <number>