Scala 3 capabilities and Tagless Final

This question is going to be a little vague and hand-wavy. I really don’t know where else to ask though, as capabilities seems to be an arcane topic still.

I’m going to phrase a lot of the following as assertions. They’re not statements that I know to be correct, but what I think I understand at the time of writing. Any and all of them might be wholly incorrect.

Simplifying things to the extreme, Scala 3 tracks effects in its so called direct-style using capabilities - values passed to an effectful function that know how to handle a given effect. Console for the effect can print to stdout, say. The type of such an effectful computation is then Console ?=> A.

There has been some work on context functions that makes their manipulation convenient, and you end up being able to write programs in a way that is much closer to what “regular” imperative programs look like. You are also able to manipulate program as values in a way that is really rather comfortable, as you can easily combine smaller programs together to write much more complex ones.

You do lose one thing that’s quite nice when using a monadic encoding of effects: it allows you to decide what your program will be interpreted as. Depending on the handler you use, you might be able to interpret an expression as an A (using Id[A] = A), as a pretty-printed string (using Pretty[A] = String), …

This is both a strength and a weakness of course, because wrapping the output of your programs in some F is exactly what makes this encoding cumbersome and requires you to jump through so many hoops to compose sub-programs. Still, it’s nice to have a choice in the representation format.

Playing with this problem, you can quickly land on the idea that you merely need to make your capabilities polymorphic to recover this ability: Console[F] ?=> F[A] for some type constructor F, for example.

And that is exactly Kyseliov’s Tagless Final encoding, where Console is what he calls a symantic.

Taking a small step back, the non-polymorphic capabilities seem to be exactly the lesser, first draft of a final embedding described in 2.1 Initial and Final embeddings - the one that doesn’t quite solve the expression problem yet.

After all that, I guess my question is: I’m seeing a rather direct correspondence between capabilities and the tagless final embedding. Am I seeing things? Is there something I failed to understand in either that makes my intuition completely wrong? And if not, is there any sort of concrete usefulness in this relationship?

4 Likes