Martin Odersky
Two weeks ago I was in Amsterdam, where we had the Scala Symposium as part of the SPLASH conference. I gave a talk at the symposium and then later on a keynote at the main conference. I had a great time, staying in a hotel on one of Amsterdam’s lovely canals and commuting by bike to the conference center. Amsterdam is a fantastic city for biking. Each day I picked another route along a different canal, and the route generally could not be long enough for me (I missed a couple of talks because of that). I noted that it’s important to always stick to the traffic rules, for instance to give way to traffic coming from the right, or you would get into an accident between two bicycles; there are so many of them around.
SPLASH is a set of conferences running together (OOPSLA being one of the main ones), so you get exposed to a variety of topics and get to talk to people from many different areas. One talk that stood out for me was Simon Peyton Jones speaking about how they are reforming the UK curriculum to teach computational thinking to kids from primary school on. It’s been Simon’s main “other” occupation besides Haskell and he gave a fascinating talk that conveyed his great enthusiasm for the cause of teaching computing the right way to every kid. His message was that we have to act now, when things are waiting to be defined. A quote: “We know we have failed if, 10 years from now, the outcome is just that every kid can code Java”.
At the Scala Symposium I spoke about how we implemented higher-kinded types in Dotty. This was a long and often painful journey. In total we tried four different approaches. Each of them was an effort of many weeks – sometimes several months – to implement the new scheme, debug it, and then finally discard it because we found out it was too hard to get right, or did not otherwise live up to expectations.
The original reason for trying so many different avenues had to do with DOT, which is intended to be the foundation of future Scala. DOT as-is has no provision for higher-kinded types, but it turns out that a restricted version of higher-kinded types can be straightforwardly encoded in it. That issue is not just academic because the dotty compiler uses DOT’s constructs as its core data structures. So what is hard to do in DOT tends to be hard to implement in the compiler as well.
Originally, we played with the idea to restrict higher-kinded types to
just the kind of partial applications that can be conveniently
encoded in DOT or dotty. The main problem was that this would have
forced us to restrict the Scala language. More advanced idioms, such
as type classes for Monad and Functor would have required rewrites
and would not be as convenient to use. The boundary between what was
expressible and what was illegal was also not very intuitive. For instance,
one could define an abstract polymorphic subtype of Maps in the usual way:
type M[K, V] <: Map[K, V]
But one could not define a type where the parameters were reversed. I.e.
type M[V, K] <: Map[K, V]
would have been illegal.
To address these limitations, we then played with two more complicated encodings of higher-kinded types in dotty’s core types. Neither of these worked out very well so in the end we settled for the “brute force” approach of adding higher-kinded types without trying to re-use most of the core. All these attempts are described in the paper Implementing Higher-Kinded Types in Dotty. The talk was not recorded but I have uploaded the slides.
Another interesting development was that after the talk I got together with Sandro Stucki and Guillaume Martres and we hashed out a slight extension of DOT, which would make it much more convenient for more advanced dependent type programming and, as a side effect, would make it quite suitable to express higher-kinded types as well. If this works out it would be a case where compiler hacking influenced the way we do theory. It’s usually more efficient to do theory first and implement it systematically once it’s done, but sometimes going from practice to theory is the only route available.