1. We are here at Scala Days 2012 in London, I’m sitting here with Miles Sabin, so Miles who are you?
Well I’m Miles Sabin, I am one of the founding partners of Underscore Consulting, previously I have been Chuusai, which is a Scala Consulting Company, I have been running since about 2008. At various times I have been responsible for the Scala IDE for Eclipse Project and I believe I have been using Scala in one way or another since about 2004. So I’m kind of like one of those people you occasionally see advertised for thirty years of Java experience, I’m almost one of those people with respect to Scala, not quite it’s a few around outside of EPFL and outside of Martin who used Scala for a little bit longer than me, but not very many.
2. So at Underscore what are your responsibilities, what do you do?
Well, to some extent I’m carrying over what I have been doing with my previous business as a component of Underscore's offering. At the moment that's primarily training and also some consulting, in the training I specialize in the more advanced end of the spectrum particularly focusing on the Scala Type System, and that is where I have very interesting things to say to people and am I think able to give a good entry point into the kinds of things that can be done with Type Systems, that’s are both useful and practical, but maybe not quite so familiar to people as you might expect.
I think it’s a bit of both, so it’s both understanding what Types can do for you and also understanding how that plays out specifically in a context of the Scala Type System. The Scala Type System has some unusual and innovative features; many things that you find in Scala's Type System you will find in other Programming Languages but it most certainly has some particular features that you really won't find anywhere else, certainly not in any even faintly mainstream Programming Language. I think Scala's inclusion of a particular form of dependent Types, I think is enormously important and it’s something that is, you really don’t find anywhere outside of academic Programming Languages.
That might sound scary but I think the key point, key thing that dependent Types bring to the table is the ability to express more and more properties of your programs in a way which it’s possible for compilers to statically check and verify, so things beyond the sort of the simple forms of type checking that you expect any reasonably modern statically typed programming language to be able to enforce, like for example that every element of list of String is a String, that is something you expect to be able to express in Java or in C#, more or less any statically typed programming language, and the ability to express the fact that a list has at least one member is a much more interesting kind of property and being able to do so in a way which can be statically verified by a compiler, so that rather than risking a runtime error by for example attempting to take the head of an empty list, you can know up front at compile time that such a thing could never ever happen.
This is something which I think is an enormously important feature of the next up and coming generation of programming languages which incorporate in either direct or indirect forms as some aspects of dependent typing.
Somewhat indirectly, the form of dependent types that Scala has, it manifest as a form of member typing so a nested type in Scala is unlike in Java or C# it isn’t owned by the enclosing type, it’s owned by the enclosing instance, so you can think of a nested type as being somehow rather a function of the instance that it is a member of, so that gives you enough material in a programming language to be able to express much more interesting and sophisticated properties, the actual mechanism that you would use to encode the fact that the list had a particular number of elements, it’s an encoding, but it can be done in such a way that as far as a sort of enduser using code which is relying on those properties, does not see too much in a way of the mechanics involved and the place to look for examples on how that's done is the OpenSource projects and I’ve been working on for over a year now, but it has more recently manifested itself as a library, Github project, Mailing List, as "Shapeless". Over the last five or six months I guess, that will be a good canonical place to go, look for an implementation of size dependent types of collections.
5. So Shapeless is basically a project for creating collections or types?
That is one part of what is involved in Shapeless, the main headline is that what I’m trying to do is explore ways in which Scala’s type system is able to express much more general kinds of polymorphism than the ones that are familiar, so more general than subtype polymorphism that you see in OOP languages or more general than the parametric polymorphism that you see in typical Functional Programming Languages, and the term that is often applied to it is generic programming or polytypic Programming. You can see manifestations of this kind of stuff both in some of the interesting new dependently typed Programming Languages like Idris or Agda and you can also see it, there are a lot of things that you can do in Haskell for example, to capture some of the same kinds of ideas and some of the very generic kind of approaches that are used to also captured in things like Template Haskell. So Shapeless abstracts over the shape of a data type, so Shapeless is intended to convey the idea that there is no one particular set of shapes that I'm intending to deal with, I try to abstract over a shape.
In terms of what kinds of things you would find in Shapeless, I should emphasize this, this is an entirely experimental project, it’s a library, you can use it, there are binary artifacts on Maven central now but it's not intended as anything other than really a collection of well worked out experiments in sort of stretching the Scala type system as far as it can possibly go. Amongst the things that you will find in there is the idea of Collections which encode their sizes, you will find heterogenous lists, for example list which are able to capture the idea of each element of the list having a potentially different type in a way which can be tracked by the type system, in a way in which operations indexing into that list will preserve type.
So if I have a heterogenous list which contains an an Integer, a String, and a Boolean, if I pick out the second element of it the compiler will know that it’s a String, but that something will be enforceable at compile time in a way that the equivalent monotypic list would not be able to capture, it would have to find some common super type of all the elements, you would lose precision by indexing into a list in that way, so these things are known as HLists, that is sort of a nod in the direction of their origins in Haskell, the H is for Heterogenous not Haskell, but the original design of these things come from work that was done with Haskell. So Hlists; heterogenous maps is another interesting kind thing; the general technologies involved in making these things work are related, heterogenous maps are going to allow you to express the idea of - similar to a map everyone's familiar with - but where the type of values is determined by the type of keys.
So for example you could specify a heterogenous map, which maps String keys to Integer values and Boolean keys to Double values or something along those lines, and again in a way that can be enforced by the compiler statically so you would know if you look up a value using a String key, you are guaranteed to get an Integer value as a result, and again in a way which can never go wrong, so you can avoid having to do either pattern matching or type testing of any sort to end up with an actual concrete type that you can work with.
6. So it's indexed on the key, the type of the key not on the value of the key?
So it’s indexed on both, so the relationship between the key types and the value types is enforced entirely at the type level but the actual individual values are going to be mapped individual, individual key instances are going to be mapped to individual values.
Actually that can be done, in a way what you are doing there is you actually encoding an idea of, if you like, first class records where you're actually using Strings in a way analogous to the names of members of a first class type, it is actually possible to encode that in Scala and there is an extensible records experiment in Shapeless which demonstrates that, and a way that you can actually make that working in Scala is by exploiting another one of Scala’s, not unique but certainly somewhat uncommon type system features known as Singleton Types, so a Singleton Type is a very, very precise type, it's the type of a particular instance.
So if you can imagine encoding keys as very specific values, then you can map the most specific type of that key to a particular type so you could map, you can’t actually strictly speaking with "Foo" or "Bar" at the moment, but you can do something very, very similar, so you can have a representative of a Foo key or a Bar key, and then have that map to a String or an Integer or something on the value side. Just in exactly the same way that you might expect to be able to set up a record or a case class in the Scala with a named member which names its value of a particular time. You can ask what is this kind of thing useful for, and generally obviously you are not going to use this kinds of things to work with when you actually have those facilities available to you as first class constituents of the language, but there are cases where you might actually need, you might want to preserve static type safety, but have a certain some more flexibility, the kind of flexibility you would only get by exploiting code generation or macros. You might for example want to match up a database schema or an XML schema or something along those lines to a record in a way which is capturable by a compiler.
This is something that you can use this kind of technique to do and again is not something that I would necessarily recommended people instantly rush out and put into production in their new object relational mapping scheme but nevertheless the techniques involved in doing that and the way in which they're are embedded in Scala I think are very important, and I think people will build production quality tools based on the kinds of ideas that are involved here. And again I think it’s another, the techniques involved, that particular example would be a combination of using Singleton Types in Scala with dependent types in Scala. It’s very powerful set of tools to have in your toolbox; there are a huge number of things that can be done with this kind of thing.
Miles Sabin: It's not entirely an obstacle but it's certainly something which makes Shapeless less practical to use than it might be otherwise. The way in which the properties that the first part of the library needs to verify are implemented by the compiler, they involve using Scala implicit values to encode properties and roughtly speaking what happens is, if for example you try to prove that the nth element of the heterogenous list is a String, you have to kind of recursively construct this sort of proof term, this witness, the compiler is able to do this at compile time. So it’s going to type check that it is able to produce an implicit object which verifies which could only be produced if the nth elements of the heterogenous list have the right type. However it's very computationally expensive at compile time for the compiler to do this, because it’s exploiting aspects of the way in which Scala’s type inference and implicit search mechanism works. It’s not optimal if you were to have heterogenous lists as a first class part of the language you would do things differently, in a way that was much more effective.
Perhaps slightly worse than that, these proof terms if you were to work in a language which did this kind of thing natively, so for example Agda or Idris, you would expect those proof terms to only exist at a compile time, they would be erased, this is a case situation where type erasure is a very, very good thing, you don’t want these proof terms to have to actually survive the compilation process and still be present at runtime. They are currently still present at runtime, so there is not a huge overhead but there is an overhead involved in producing these largely useless runtime artifacts, which are only there because they needed to be present at compile time.
Now it turns out that Scala Macros are going to make it possible to, if you like, have a little escape hatch out of the compiler’s normal compilation process, they basically magic these proof terms into existence at compilation time and in a way which means that it should be possible to completely eliminate any runtime residue of those things. So I think probably for that reason and many more, I'm very keen to see macros arrive in Scala. It’s interesting, macros, some people see them as being a sort of way of escaping from the type system, it’s often said that you know, languages grow macros systems when they find their type systems are not quite expressive enough, and I think there is some truth in that but I think in this particular case there are many, many things that I think we can usefully do with macros in Scala which I actually don’t fall into that category, I think the idea of using macros as a mechanism for actually say erasing proof terms in Scala programs, I think that is very, very interesting indeed. So yes, macros, that is what I’m looking for too.
Werner Schuster: It seems like everybody is talking about macros in nowadays, so it seems to be an interesting feature for the future.
Miles Sabin: Sure.
9. To wrap up, our special Scala Days question. Miles Sabin describe yourself as a Monad.
Miles Sabin: I think I will be the Continuation Monad, because I`m going to carry on, and on and on doing these kind of stuff until I`ve reached some kind of type level nirvana and...
Werner Schuster: ... you transform into an Exception Monad.