Literally dependent types

Given that the formalization of Scala Classic has ground to a halt, for reasons I may go into later, I spent part of today hacking on the Scala compiler itself to add support for singleton literals. Currently, Scala allows singleton types for stable identifiers. My modification allows literals to be used in singleton types. I can't promise that it will be in the forthcoming Scala 2.7.2 release, but I would like it to be.

Overall it was far less work than I was expecting.  Scala already internally supports what it calls "constant types", there is just no way to write them in Scala source code presently.  Consequently, most of the effort was in extending the parser.

Given my modifications, it is now possible to write code like the following:

  2. scala> val x : "foo".type = "foo"
  3. x: "foo".type = foo

What I was not expecting was that out-of-the-box things like the following would work:

  2. scala> val x : "foobar".type = "foo" + "bar"
  3. x: "foobar".type = foobar
  4. scala> val y : 10.type = 2 * 5
  5. y: 10.type = 10
  6. scala> def frob(arg : 10.type) : 6.type = arg - 4
  7. frob: (10.type)6.type

Unfortunately the excitement soon passes when you realize all the things you can't do with singleton literals (yet). Even if we turn on the experimental dependent method support, you can't write things like

  2. def add(arg : Int) : (arg + 5).type = arg + 5

because these are exactly what they are called, singleton literals, not full-blown dependent types.

One cute example, based on a use suggested by Sean McDirmid, would be that some people might do something like the following with implicits:

  2. implicit stringToColor(arg : String) : java.awt.Color = java.awt.Color.getColor(arg)

However, with singleton literals you can tighten it up by ensuring that for some strings it will never fail:

  2. implicit redToColor(arg : "red".type) : java.awt.Color = java.awt.Color.RED
  3. implicit blueToColor(arg : "blue".type) : java.awt.Color = java.awt.Color.BLUE

Happily, the type inferencer already chooses the most specific implicit conversions.

In any event, they will hopefully become more useful as the type system continues to grow. I am also sure someone will probably come up with a clever use for them that hasn't occurred to me yet. If so, let me know.

Comments (5)