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:

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

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

  1.  
  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
  8.  

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

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

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:

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

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

  1.  
  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
  4.  

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.

5 Comments »

  1. David R. MacIver said,

    July 22, 2008 @ 2:25 am

    So I was tinkering with the idea and trying to come up with a use for it. I’ve been struggling a bit – it doesn’t look like a very useful feature on its own (though it looks like it leads in some interesting directions).

    One thing that occurred to me for making this more useful is if the value of the singleton type were available as an implicit value. I suspect this causes problems though, because it’s then also available as an implicit value of the supertype. An example use case was the ranged types implementation I was tinkering with a while ago. If the values were available implicitly then you could also make a range object available implicitly. It’s a bit of a stretch though.

    Another thing I was wondering about: How will this interact with the type inferencer? e.g. if I write

    def foo = “foo”;

    presumably foo will be inferred as returning a String, not a “foo”.type? How does this work with the normal approach of always inferring the most specific type? Otherwise you’re going to have to use a lot more type annotations than you used to (for cases where foo should be overrideable, or where it’s actually a var)

    The other part of the reason I ask is that sometimes you’d actively want the most specific type to be inferred. e.g. I was wondering about using this as an alternative to Enumeration, so you could define something like

    val Months = “January” | “February” | etc.

    and statically check membership of string literals. But this becomes really crappy to use if the literals are inferred as type String as you end up having to provide all the type parameters (though this could also work not too badly with the implicits suggestion)

    Anyway, just some random thoughts.

  2. washburn said,

    July 22, 2008 @ 9:51 am

    @David: No, def foo will get type String. For better or worse, Scala already does not infer the the most specific type in many cases. In fact, in most of the time it will throw away singleton types and replace them with their underlying type, even if you try adding more annotations than is desirable (see ticket #837).

    I had briefly thought about the enumeration example, but I couldn’t see a good way to make it work without union types. We could potentially add union types in the future, but the theory needs to be verified first.

  3. David R. MacIver said,

    July 22, 2008 @ 11:19 am

    Yeah. I thought I could fake union types with some appropriate combination of implicits to handle embeddings, but after some experimentation I can’t appear to coerce the type checker into resolving the embeddings correctly, so the enumerations idea doesn’t work after all. Sorry.

  4. Denys said,

    October 30, 2014 @ 5:14 pm

    Hi there,

    It looks Scala might finally get those in upcoming SIP-23: http://docs.scala-lang.org/sips/pending/42.type.html

    Discussion of the latest implementation here: https://groups.google.com/d/msg/scala-internals/Ny9s6Aq7ThI/rLlGTKtL7W8J

    Cheers,
    Denys

  5. washburn said,

    October 31, 2014 @ 3:07 pm

    @Denys Cool, though it looks like the proposal doesn’t cover any automated reasoning about equivalences. So it will be necessary to use explicit equality witnesses.

RSS feed for comments on this post · TrackBack URI

Leave a Comment