SIP-23 - Literal-based singleton types

Authors: George Leontiev, Eugene Burmako, Jason Zaugg, Adriaan Moors, Paul Phillips, Oron Port, Miles Sabin

Supervisor and advisor: Adriaan Moors

History

Introduction

Singleton types, types which have a unique inhabitant, have been a fundamental component of Scala’s semantics dating back to the earliest published work on its type system. They are ubiquitous in ordinary Scala code, typically as the types of Scala object definitions understood as modules, where their role is to give the meaning of paths selecting types and terms from nested values. Selector paths have an intuitive meaning to programmers from a wide range of backgrounds which belies their underpinning by a somewhat “advanced” concept in type theory.

Nevertheless, by pairing a type with its unique inhabitant, singleton types bridge the gap between types and values, and their presence in Scala has, over the years, allowed Scala programmers to explore techniques which would typically only be available in languages such as Agda or Idris, with support for full-spectrum dependent types.

Scala’s semantics have up until now been richer than its syntax. The only singleton types which are currently directly expressible are those of the form p.type where p is a path pointing to a value of some subtype of AnyRef. Internally the Scala compiler also represents singleton types for individual values of subtypes of AnyVal, such as Int or values of type String, which don’t correspond to paths. These types are inferred in some circumstances, notably as the types of final vals. Their primary purpose has been to represent compile-time constants (see 6.24 Constant Expressions and the discussion of “constant value definitions” in 4.1 Value Declarations and Definitions). The types here correspond to literal values (ie. values which programmers can directly write as terms, see 1.3 Literals) such as 23, true or "foo" of the larger non-singleton types they inhabit (Int, Boolean or String respectively). However, there is no surface syntax to express these types.

As we will see in the motivation section of the proposal below, singleton types corresponding to literal values (henceforth literal types) have many important uses and are already widely used in many important Scala libraries. The lack of first class syntax for literal types has forced library authors to use the experimental Scala macro system to provide a means to express them. Whilst this has proved to be extremely successful, it has poor ergonomics (although this can typically be hidden from library users) and is not portable – because Scala macros in general and the mechanisms used to expose literal types to Scala programs in particular depend on internal implementation details of the current Scala compiler.

The poor ergonomics of macro-based exposure of literal types was the original motivation for this SIP. The development of Dotty and other Scala dialects since then has made the portability issue more urgent.

Implementation status

Literal types have been implemented in both Typelevel Scala and Dotty.

There has been a great deal of useful experience with the Typelevel Scala implementation in a variety of projects which has resulted in several improvements which are incorporated in the latest iteration of this document. A full implementation of this proposal exists as a pull request relative to the 2.13.x branch of the Lightbend Scala compiler.

Proposal

Proposal summary

• Literals can now appear in type position, designating the corresponding singleton type.

  val one: 1 = 1                     // val declaration
  def foo(x: 1): Option[1] = Some(x) // param type, type arg
  def bar[T <: 1](t: T): T = t       // type parameter bound
  foo(1: 1)                          // type ascription
  

• The .type singleton-type-forming operator can be applied to values of all subtypes of Any. To prevent the compiler from widening our return type, we assign to a final val.

  def foo[T](t: T): t.type = t
  final val bar = foo(23)            // result is bar: 23
  

• The presence of an upper bound of Singleton on a formal type parameter indicates that singleton types should be inferred for type parameters at call sites. To help see this, we introduce type constructor Id to prevent the compiler from widening our return type.

  type Id[A] = A
  def wide[T](t: T): Id[T] = t
  wide(23)                           // result is 23: Id[Int]
  def narrow[T <: Singleton](t: T): Id[T] = t
  narrow(23)                         // result is 23: Id[23]
  

• Pattern matching against literal types and isInstanceOf tests are implemented via equality/identity tests of the corresponding values.

  (1: Any) match {
    case one: 1 => true
    case _ => false
  }                                  // result is true: Boolean
  (1: Any).isInstanceOf[1]           // result is true: Boolean
  

• A scala.ValueOf[T] type class and corresponding scala.Predef.valueOf[T] operator has been added, yielding the unique value of types with a single inhabitant.

  def foo[T](implicit v: ValueOf[T]): T = v.value
  foo[13]                            // result is 13: Int
  

Motivating examples

Many of the examples below use primitives provided by the Scala generic programming library shapeless. It provides a Witness type class and a family of Scala-macro-based methods and conversions for working with singleton types and shifting from the value to the type level and vice versa. One of the goals of this SIP is to enable Scala programmers to achieve similar results without having to rely on a third party library or fragile and non-portable macros.

The relevant parts of shapeless are excerpted in Appendix 1. Given the definitions there, some of the forms summarized above can be expressed in current Scala,

val wOne = Witness(1)
val one: wOne.T = wOne.value  // wOne.T is the type 1
                              // wOne.value is 1: 1

def foo[T](implicit w: Witness[T]): w.T = w.value
foo[wOne.T]                   // result is 1: 1

"foo" ->> 23      // shapeless record field constructor
                  // result type is FieldType["foo", Int]

The syntax is awkward, and hiding it from library users is challenging. Nevertheless they enable many constructs which have proven valuable in practice.

shapeless records

shapeless models records as HLists (essentially nested pairs) of record values with their types tagged with the singleton types of their keys. The library provides user-friendly mechanisms for constructing record values, however it is extremely laborious to express the corresponding types. Consider the following record value,

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

Using shapeless and current Scala, the following would be required to give book an explicit type annotation,

val wAuthor = Witness("author")
val wTitle = Witness("title")
val wId = Witness("id")
val wPrice = Witness("price")
type Book =
  (wAuthor.T ->> String) ::
  (wTitle.T  ->> String) ::
  (wId.T     ->> Int) ::
  (wPrice.T  ->> Double) ::
  HNil

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

Notice that here the val definitions are essential – they are needed to create the stable path required for selection of the member types T.

Under this proposal we can express the record type directly,

type Book =
  ("author" ->> String) ::
  ("title"  ->> String) ::
  ("id"     ->> Int) ::
  ("price"  ->> Double) ::
  HNil

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

shapeless enables generic programming and type class derivation by providing a mechanism for mapping a value of a standard Scala algebraic data type onto a sum of products representation type, essentially nested labelled Eithers of the records discussed above. Techniques of this sort are widely used, and removing the incidental complexity that comes with encoding via macros will improve the experience for many users across a wide variety of domains.

refined and singleton-ops

refined and singleton-ops are two libraries which build on shapeless’s Witness to support refinement types for Scala. A refinement is a type-level predictate which constrains a set of values relative to some base type, for example, the type of integers greater than 5.

refined allows such types to be expressed in Scala using shapeless’s Witness,

val w5 = Witness(5)
val a: Int Refined Greater[w5.T] = 10

// Since every value greater than 5 is also greater than 4,
// `a` can be ascribed the type Int Refined Greater[w4.T]:
val w4 = Witness(4)
val b: Int Refined Greater[w4.T] = a

// An unsound ascription leads to a compile error:
val w6 = Witness(6)
val c: Int Refined Greater[w6.T] = a

//<console>:23: error: type mismatch (invalid inference):
// Greater[Int(5)] does not imply
// Greater[Int(6)]
//       val c: Int Refined Greater[W.`6`.T] = a
                                             ^

Under this proposal, we can express these refinements much more succinctly,

val a: Int Refined Greater[5] = 10

val b: Int Refined Greater[4] = a

Type-level predicates of this kind have proved to be useful in practice and are supported by modules of a number of important libraries.

Experience with those libraries has led to a desire to compute directly over singleton types, in effect to lift whole term-level expressions to the type level, which has resulted in the development of the singleton-ops library. singleton-ops is built with Typelevel Scala, which allows it to use literal types, as discussed in this SIP.

import singleton.ops._

class MyVec[L] {
  def doubleSize = new MyVec[2 * L]
  def nSize[N] = new MyVec[N * L]
  def getLength(implicit length : SafeInt[L]) : Int = length
}
object MyVec {
  implicit def apply[L]
    (implicit check : Require[L > 0]) : MyVec[L] =
       new MyVec[L]()
}
val myVec : MyVec[10] = MyVec[4 + 1].doubleSize
val myBadVec = MyVec[-1] //fails compilation, as required

singleton-ops is used by a number of libraries, most notably our next motivating example, Libra.

Libra

Libra is a a dimensional analysis library based on shapeless, spire and singleton-ops. It support SI units at the type level for all numeric types. Like singleton-ops, Libra is built using Typelevel Scala and so is able to use literal types, as discussed in this SIP.

Libra allows numeric computations to be checked for dimensional correctness as follows,

import spire.implicits._
// import spire.implicits._

import libra._, libra.si._
// import libra._
// import libra.si._

(3.m + 2.m).show
// res0: String = 5 m [L]

(3.m * 2.m).show
// res1: String = 6 m^2 [L^2]

(1.0.km.to[Metre] + 2.0.m + 3.0.mm.to[Metre]).show
// res2: String = 1002.003 m [L]

(3.0.s.to[Millisecond] / 3.0.ms).show
// res3: String = 1000.0  []

3.m + 2.kg //this should fail
// <console>:22: error: These quantities can't be added!
//        3.m + 2.kg //this should fail
//            ^

Spire

The Scala numeric library Spire provides us with another example where it is useful to be able to use literal types as a constraint.

Spire has an open issue to add a Residue type to model modular arithmetic. An implementation might look something like this,

case class Residue[M <: Int](n: Int) extends AnyVal {
  def +(rhs: Residue[M])(implicit m: ValueOf[M]): Residue[M] =
    Residue((this.n + rhs.n) % valueOf[M])
}

Given this definition, we can work with modular numbers without any danger of mixing numbers with different moduli,

val fiveModTen = Residue[10](5)
val nineModTen = Residue[10](9)

fiveModTen + nineModTen    // OK == Residue[10](4)

val fourModEleven = Residue[11](4)

fiveModTen + fourModEleven
// compiler error: type mismatch;
//   found   : Residue[11]
//   required: Residue[10]

Also note that the use of ValueOf as an implicit argument of + means that the modulus does not need to be stored along with the Int in the Residue value, which could be beneficial in applications which work with large datasets.

Proposal details

• Literals can now appear in type position, designating the corresponding singleton type. The SimpleType production is extended to include syntactic literals.

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

  Examples:

  val one: 1 = 1                     // val declaration
  def foo(x: 1): Option[1] = Some(x) // param type, type arg
  def bar[T <: 1](t: T): T = t       // type parameter bound
  foo(1: 1)                          // type ascription
  

• The restriction that the singleton-type-forming operator .type can only be appended to stable paths designating a value which conforms to AnyRef is dropped – the path may now conform to Any. Section 3.2.1 of the SLS is updated as follows,

  Singleton Types

  SimpleType  ::=  Path ‘.’ ‘type’
  

  A singleton type is of the form p.type. Where p is a path pointing to a value which conforms to scala.AnyRef, the type denotes the set of values consisting of null and the value denoted by p (i.e., the value v for which v eq p). Where the path does not conform to scala.AnyRef the type denotes the set consisting of only the value denoted by p.

  Example:

  def foo[T](t: T): t.type = t
  final val bar = foo(23)            // result is bar: 23
  

• The presence of an upper bound of Singleton on a formal type parameter indicates that singleton types should be inferred for type parameters at call sites.

  This SIP aims to leave the meaning of all currently valid programmes unchanged, which entails that it must not alter type inference in currently valid programmes. Current Scala will generally widen the types of literal values from their singleton type to their natural non-singleton type when they occur in expressions. For example in,

  val foo = 23
  def id[T](t: T): T = t
  id(23)
  

  we expect the inferred type of foo and the actual type parameter inferred for T in the application of id to both be Int rather than 23. This behaviour seems to be natural and appropriate in circumstances where the programmer is not deliberately working with singleton types.

  With the introduction of literal types, however, we do want to be able to infer singleton types in cases such as these,

  case class Show[T](val s: String)
  object Show {
    implicit val showTrue: Show[true] = Show[true]("yes")
    implicit val showFalse: Show[false] = Show[false]("no")
  }
  
  def show[T](t: T)(implicit st: Show[T]): String = st.s
  show(true)   // currently rejected
  

  The proposal in this SIP is that we use an upper bound of Singleton on a formal type parameter to indicate that a singleton type should be inferred. The above example would then be written as,

  def show[T <: Singleton](t: T)
    (implicit st: Show[T]): String = st.s
  show(true)  // compiles and yields "yes"
  

  This change will not affect the meaning of currently valid programmes, because the widened types inferred for literal values at call sites do not currently conform to Singleton, hence all call sites of the form in the above example would currently be rejected as invalid.

  Whilst type inference in Scala is not fully specified, section 6.26.4 Local Type Inference contains language which explicitly excludes the inference of singleton types (see cases 2 and 3, “None of the inferred types Ti is a singleton type”). This does not match the current Scala or Dotty compiler implementations, where singleton types are inferred where a definition is final, specifically non-lazy final val definitions and object definitions. Where a definition has had a singleton type inferred for it, singleton types will be inferred from its uses,

  final val narrow = 23      // inferred type of narrow: 23
  
  class Wide
  object Narrow extends Wide
  def id[T](t: T): T = t
  id(Narrow)                 // result is Narrow: Narrow.type
  

  This SIP updates the specification to match the current implementation and then adds the further refinement that an explicit upper bound of Singleton indicates that a singleton type should be inferred.

  Given,

  A singleton-apt definition is

  1. An object definition, or
  2. A non-lazy final val definition

  the relevant clauses of 6.26.4 are revised as follows,

  None of the inferred types Ti is a singleton type unless, (1) Ti is a singleton type corresponding to a singleton-apt definition, or (2) The upper bound Ui of Ti conforms to Singleton.

  Example:

  type Id[A] = A
  def wide[T](t: T): Id[T] = t
  wide(23)                           // result is 23: Id[Int]
  def narrow[T <: Singleton](t: T): Id[T] = t
  narrow(23)                         // result is 23: Id[23]
  

  Note that we introduce the type constructor Id simply to avoid widening of the return type.

• A scala.ValueOf[T] type class and corresponding scala.Predef.valueOf[T] operator has been added, yielding the unique value of types with a single inhabitant.

  Type inference allows us to infer a singleton type from a literal value. It is natural to want to be able to go in the other direction and infer a value from a singleton type. This latter capability was exploited in the motivating Residue example given earlier, and is widely relied on in current Scala in uses of shapeless’s records, and LabelledGeneric-based type class derivation.

  Implicit resolution is Scala’s mechanism for inferring values from types, and in current Scala, shapeless provides a macro-based materializer for instances of its Witness type class. This SIP adds a directly compiler-supported type class as a replacement:

  final class ValueOf[T](val value: T) extends AnyVal
  

  Instances are automatically provided for all types with a single inhabitant, which includes literal and non-literal singleton types and Unit.

  Example:

  def foo[T](implicit v: ValueOf[T]): T = v.value
  foo[13]                            // result is 13: Int
  

  A method valueOf is also added to scala.Predef, analogously to existing operators such as classOf, typeOf etc.

  def valueOf[T](implicit vt: ValueOf[T]): T = vt.value
  

  Example:

  object Foo
  valueOf[Foo.type]       // result is Foo: Foo.type
  
  valueOf[23]             // result is 23: Int
  

• Pattern matching against literal types and isInstanceOf tests are implemented via equality/identity tests of the corresponding values.

  Pattern matching against typed patterns (see 8.1.2 Typed Patterns) where the TypePat is a literal type is translated as a match against the subsuming non-singleton type followed by an equality test with the value corresponding to the literal type.

  Where applied to literal types, isInstanceOf is translated to a test against the subsuming non-singleton type and an equality test with the value corresponding to the literal type.

  Examples:

  (1: Any) match {
    case one: 1 => true
    case _ => false
  }                                  // result is true: Boolean
  (1: Any).isInstanceOf[1]           // result is true: Boolean
  

  Importantly, that doesn’t include asInstanceOf, as that is a user assertion to the compiler, with the compiler inserting in the generated code just enough code for the underlying runtime to not give a ValidationError. The compiler should not, for instance, generate code such that an expression like (1: Any).asInstanceOf[2] would throw a ClassCastException.

• Default initialization for vars with literal types is forbidden.

  The default initializer for a var is already mandated to be its natural zero element (0, false, null etc.). This is inconsistent with the var being given a non-zero literal type:

  var bad: 1 = _
  

  Whilst we could, in principle, provide an implicit non-default initializer for cases such as these, it is the view of the authors of this SIP that there is nothing to be gained from enabling this construction, and that default initializer should be forbidden.

Follow-on work from this SIP

Whilst the authors of this SIP believe that it stands on its own merits, we think that there are two areas where follow-on work is desirable, and one area where another SIP might improve the implementation of SIP-23.

Infix and prefix types

SIP-33 Match Infix and Prefix Types to Meet Expression Rules has emerged from the work on refined types and computation over singleton types mentioned in the motivation section above.

Once literal types are available, it is natural to want to lift entire expressions to the type level as is done already in libraries such as singleton-ops. However, the precedence and associativity of symbolic infix type constructors don’t match the precedence and associativity of symbolic infix value operators, and prefix type constructors don’t exist at all. It would be valuable to continue the process of aligning the form of the types and terms.

Byte and short literals

Byte and Short have singleton types, but lack any corresponding syntax either at the type or at the term level. These types are important in libraries which deal with low-level numerics and protocol implementation (see eg. Spire and Scodec) and elsewhere, and the ability to, for instance, index a type class by a byte or short literal would be valuable.

A prototype of this syntax extension existed at an early stage in the development of Typelevel Scala, but never matured. The possibility of useful literal types adds impetus.

Opaque types

In the reference implementation of SIP-23, the ValueOf[A] type is implemented as a value class. This means that implicit evidence of ValueOf[A] will erase to A (the value associated with the singleton types). This is desirable, but due to value class restrictions, ends up boxing primitive types (such as Int).

If we implemented ValueOf[A] as an opaque type instead of a value class, then this boxing would be elided, and the valueOf[A] method would be compiled to an identity function.

Related Scala issues resolved by the literal types implementation

• SI-1273 Singleton type has wrong bounds
• SI-5103 Singleton types not inferred in all places they should be
• SI-8323 Duplicate method name & signature with singleton type parameters over constant types
• SI-8564 Methods with ConstantType results get the inhabitant of ConstantType as their body

Appendix 1 – shapeless excerpts

Extracts from shapeless relevant to the motivating examples for this SIP:

trait Witness {
  type T           // the singleton type represented by this Witness
  val value: T {}  // the unique inhabitant of that type
}

object Witness extends Dynamic {
  type Aux[T0] = Witness { type T = T0 }
  type Lt[Lub] = Witness { type T <: Lub }

  /**
   * Materialize the Witness for singleton type T
   */
  implicit def apply[T]: Witness.Aux[T] = macro ...

  /**
   * Convert a literal value to its Witness
   */
  implicit def apply[T](t: T): Witness.Lt[T] = macro ...
}

object labelled {
  /**
   * The type of fields with keys of singleton type `K` and value type `V`.
   */
  type FieldType[K, +V] = V with KeyTag[K, V]
  trait KeyTag[K, +V]

  /**
   * Yields a result encoding the supplied value with the singleton type `K' as its key.
   */
  def field[K] = new FieldBuilder[K]

  class FieldBuilder[K] {
    def apply[V](v : V): FieldType[K, V] = v.asInstanceOf[FieldType[K, V]]
  }
}

object singleton {
  implicit def mkSingletonOps(t: Any): SingletonOps = macro ...
}

trait SingletonOps {
  import labelled._

  type T

  /**
   * Returns a Witness of the singleton type of this value.
   */
  val witness: Witness.Aux[T]

  /**
   * Narrows this value to its singleton type.
   */
  def narrow: T {} = witness.value

  /**
   * Returns the provided value tagged with the singleton type
   * of this value as its key in a record-like structure.
   */
  def ->>[V](v: V): FieldType[T, V] = field[T](v)
}