SIP-23 - Literal-based singleton types

By: George Leontiev, Eugene Burmako, Jason Zaugg, Adriaan Moors, Paul Phillips

Note: This SIP is considered a “good idea”, but is a work-in-process. There is no guarantee that it will not be dropped if at some point it is decided that its foundation is not good enough.

Champion: Adriaan Moors

Last update: July 15, 2014

Motivation

Singleton types bridge the gap between the value level and the type level and hence allow the exploration in Scala of techniques which would typically only be available in languages with support for full-spectrum dependent types.

Scala’s type system can model constants (e.g. 42, "foo", classOf[String]). These are inferred in cases like object O { final val x = 42 }. They are used to denote and propagate compile time constants (See 6.24 Constant Expressions and discussion of “constant value defintion” in 4.1 Value Declarations and Definitions). However, there is no surface syntax to express such types. This makes people who need them, create macros that would provide workarounds to do just that (e.g. shapeless). This can be changed in a relatively simple way, as the whole machinery to enable this is already present in the scala compiler.

Another motivation for adding this functionality is the fact that it is already partially available in scala, but the way it is available makes interaction with this feature a bit inconsistent. Here’s what is possible in the current version of scala:

scala> val t = "test"
t: String = test

scala> val r: t.type = t
r: t.type = test

But:

scala> val r: "test".type = "test"
<console>:1: error: identifier expected but string literal found.
       val r: "test".type = "test"
              ^

And:

scala> val r: 42.type = 42
<console>:1: error: identifier expected but integer literal found.
       val r: 42.type = 42
              ^

Or even:

scala> val t = 42
t: Int = 42

scala> val r: t.type = t
<console>:8: error: type mismatch;
 found   : t.type (with underlying type Int)
 required: AnyRef
       val r: t.type = t
              ^

This looks like an inconsistency, which should be fixed. The proposed change fixes exactly that:

scala> val r: "test".type = "test"
r: "test".type = test

scala> val r: 42.type = 42
r: 42.type = 42

or even:

scala> val r: 42 = 42
r: 42.type = 42

scala> val t = 42
t: Int = 42

scala> val r: t.type = t
r: t.type = 42

To summarize, scala has full support for literal-based singleton types, but language user has very limited possibilities for creating and using them. Two possible ways currently are asking the compiler to infer the singleton type by marking value as final, or use .type syntax, which is only available for stable identifiers pointing to values that conform to AnyRef.

Prerequisites

Any vs AnyRef

Currently there is a possibility to use singleton types in some contexts, but only on identifiers which point to a constant that conforms to AnyRef. This restriction is due to Any not having an eq method, which is what’s used for singleton type-equality check and pattern matching https://github.com/scala/scala/pull/3558. This has been discussed on the mailing list here and here, and there is a consent that this needs to be done.

Inhabitants of the type

Getting the inhabitant of a singleton type, as described by Travis Brown, can be done with a macro, which is a part of the proposed implementation.

Note: This is one of the many parts of this SIP that are in flux, and are likely to change in the future. We might not need to generate instances of SingleInhabitant typeclass, but instead only use <: Singleton type bound for this. See SI-5103. The name is also likely to change to valueOf[T].

Possible use cases

There are quite a few use cases we’ve collected on the mailing list. Some of them are as follows.

Spire

Singleton types will be useful for defining a type like Residue[13.type] (Z/13Z, the group of integers modulo 13). We could then mandate that residues can be added only when they are parameterized on the same number. Possibly something like:

case class Residue[N <: Int : SingleInhabitant](n: Long) { lhs =>
   def +(rhs: Residue[N]): Residue[N] =
     Residue((lhs.n + rhs.n) % inhabitant[N])
}

Another use is to help with property based testing. In Spire, there is a Ranged type that makes it easy to ask for numbers in a particular range in ScalaCheck:

forAll { x: Ranged[Int, 1, 100] =>
   val n: Int = x.value // guaranteed to be 1 to 100
}

Currently Spire just builds some of the most common number literals and uses boilerplate to define the end points of Ranged. But this is another place where singleton types could really help make things clear. Here’s what Ranged could look like:

class Ranged[From <: Int : SingleInhabitant, To <: Int : SingleInhabitant] {
    def value = {
      val rnd = new scala.util.Random
      val from = inhabitant[From]
      val to = inhabitant[To]
      (from + rnd.nextInt(to - from + 1))
  }
}

There is also all kinds of length/dimension checking and other standard cases where singleton types will help.

Scala.js

There is an important use case for literal-based singleton types in Scala.js. In particular for Strings: declaring several overloads of a method that differ only in the actual strings in parameters, for example:

trait HTMLCanvasElement extends HTMLElement {
  def getContext(contextId: String): Any
  def getContext(contextId: "2d".type): CanvasRenderingContext2D
}

so that at call-site:

val anyContext = canvas.getContext("webgl")
val context2D = canvas.getConttext("2d")

anyContext is an Any but context2D is statically known to be a CanvasRenderingContext2D.

Note: The way this currently works:

scala> :t canvas.getContext("webgl")
Any

scala> :t canvas.getContext("2d")
Any

But

scala> :t canvas.getContext("2d": "2d".type)
CanvasRenderingContext2D

Shapeless

Shapeless is a project that makes heavy use of singleton types already. It has all the machinery in place to make working with them nicer. Hence, it is a source of inspiration for working on this SIP. This change does not bring much to the table for shapeless though. One of the useful cases would be an ability to explicitly specify types for e.g. records in a more convenient way than possible with the current version of scala:

val book: "author" ->> String ::
          "title" ->> String ::
          "id" ->> Int ::
          "price" ->> Double :: HNil =
 ("author" ->> "Benjamin Pierce") ::
 ("title"  ->> "Types and Programming Languages") ::
 ("id"     ->>  262162091) ::
 ("price"  ->>  44.11) ::
 HNil

Others

Quite a few other projects find this feature relevant for more efficient work on the tasks they are solving: Slick, Spark, Scala RX, Scalding, Breeze.

Proposal

This document proposes to extend an existing very limited syntax for singleton types to a more general one. That is, possibility to use syntax for singleton types, as well as raw literals, in any type position. Here are several examples (taken from the tests):

Simple examples:

type _42 = 42.type
type Unt = ().type
type _1 = 1 // .type is optional for literals
final val x = 1
type one = x.type // … but mandatory for identifiers

This is not allowed for the reason that we will have problems bootstrapping this

scala> type _2 = (1+1).type
<console>:1: error: '.' expected but identifier found.
       type _2 = (1+1).type
                   ^

Using it with vars:

scala> var x: 3.type = 3

scala> x = 42
  <console>:8: error: type mismatch;
   found   : 42.type (with underlying type Int)
   required: 3.type
         x = 42
             ^

Pattern-matching

val y: 5 = 5

def g(x: Int) = x match {
  case _: y.type => 0
  case _: 7.type => 1
  case _         => 2
}

Etc.

trait Succ[T] {
  type Out
  def apply(x: T): Out
}

implicit object One extends Succ[1.type] {
  type Out = 2.type
  def apply(x: 1.type) = 2
}

def f[T](x: T)(implicit succ: Succ[T]) = succ(x)

def main(args: Array[String]): Unit = {
  println(f(1))
  // println(f(5))
  println((g(1), g(5), g(7)))
}

Formalization

The proposed change is essentially as follows (adding on the language reference):

SimpleType        ::=  SimpleType TypeArgs
                    |  SimpleType ‘#’ id
                    |  StableId
                    |  Path ‘.’ ‘type’
                    |  Literal [‘.’ type]
                    |  ‘(’ Types ‘)’

A singleton type is of the form p.type, where p is a path pointing to a value. Or literal[.type] (in this case .type is optional, because when using a literal we always know if we are in a type- or term-parsing mode). The type denotes set of values consisting of a single value denoted by path p, or a literal.

Implementation

The singleton type part (not including eq on Any) is implemented on github. There are currently several outstanding issues that need to be looked into. Namely, ConstantType folding and inlining of functions with singleton type result.

The places where those issues might present themselves are marked with TODO (folone), and can be found like this:

$ ack “TODO \(folone\)” src/

Other places where ConstantType is used can be found like this:

$ grep -r --include="*.scala" "ConstantType" src/

Some details on the optionality of .type

While discussing this document, the agreement was that we should keep the mandatory .type for identifiers, to avoid situations described by Adriaan Moors:

type T = Int
final val T = 1
val x: T = 2 // Which T is this: T, or T.type?

but make it optional for literals, e.g. both 42.type and 42 in type position are valid.

This change is implemented in the branch, and needs a careful update of all the failed check files (partest can do that automatically: partest --update-check).

Dependencies on other SIPs

This project needs an eq method on Any.

Weird behaviour collected so far

Inlining of functions

scala> def test: 7.type = {
     |   println("PANDA!")
     |   7
     | }
test: 7.type

scala> test
res0: 7.type = 7

Suspected culprit

Can hopefully be fixed by verifying that the body is pure (by means of SI-7656) before inlining it.

blog comments powered by Disqus

Contents