New blog post

Author: odersky

blog/_posts/2016-11-17-splash.md

@@ -0,0 +1,87 @@
+---
+layout: blog
+post-type: blog
+by: Martin Odersky
+title: SPLASH Amsterdam and Higher-kinded Types
+---
+
+Two weaks 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 reform 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 was talking about how we implemented
+higher-kinded types in Dotty. This was a long and often painful
+journey. We tried overall 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 live up otherwise 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 it is has no povision 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 hard to implement in
+the compiler as well.
+
+Originally, we played with the idea to restrict higher-kinded types to
+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 would 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 played then 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](https://infoscience.epfl.ch/record/222780/files/p51-odersky.pdf).
+The talk was not recorded but I have uploaded the
+[slides](http://www.slideshare.net/Odersky/implementing-higherkinded-types-in-dotty).
+
+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.
+
+