SIP-23 - Literal-based singleton types

Language

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

Supervisor and advisor: Adriaan Moors

History

Date Version
Jun 27th 2014 Initial SIP
Jul 15th 2014 Last update to SIP before declared dormant
TBD Dormant because original authors are not available for its review
Feb 9th 2017 New author volunteered to update the SIP for review
Nov 16th 2017 Updated following implementation experience in Typelevel Scala

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 it’s 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. Interally 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 suface 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 ergonimics (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 programmes 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.
    def foo[T](t: T): t.type = t
    foo(23)                            // result is 23: 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.
    def wide[T](t: T): T = t
    wide(13)                           // result is 13: Int
    def narrow[T <: Singleton](t: T): T = t
    narrow(23)                         // result is 23: 23
    
  • Pattern matching against literal types and isInstanceOf/asInstanceOf tests/conversions are implemented via equality/identity tests of the corresponding values.
    (1: Any) match {
      case one: 1 => true
      case _ => false
    }                                  // result is true
    (1: Any).isInstanceOf[1]           // result is true
    (1: Any).asInstanceOf[1]           // result is 1: 1
    (1: Any).asInstanceOf[2]           // ClassCastException
    
  • 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: 13
    
  • Support for scala.Symbol literal types has been added.
    valueOf['foo]                      // result is 'foo: 'foo
    

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 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 Either’s 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 thar 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 modulii,

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
    foo(23)                            // result is 23: 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 Widen
    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 explict 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,

    def wide[T](t: T): T = t
    wide(13)                           // result is 13: Int
    def narrow[T <: Singleton](t: T): T = t
    narrow(23)                         // result is 23: 23
    
  • 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 materialier 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: 13
    

    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: 23
    
  • Pattern matching against literal types and isInstanceOf/asInstanceOf tests/conversions 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 and asInstanceOf are translated to a test against the subsuming non-singleton type and an equality test with the value corresponding to the literal type. In the case of asInstanceOf a ClassCastException is thrown if the test fails.

    Examples,

    (1: Any) match {
      case one: 1 => true
      case _ => false
    }                                  // result is true
    (1: Any).isInstanceOf[1]           // result is true
    (1: Any).asInstanceOf[1]           // result is 1: 1
    (1: Any).asInstanceOf[2]           // ClassCastException
    
  • Default initialization for vars with literal types is forbidden.

    The default initializer for a var is already mandated to be it’s 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.

  • Support for scala.Symbol literal types has been added.

    The scala.Symbol type has first class syntax support, like String. Despite having syntactic literals, it does not have semantic literals in the same way that String does. This SIP adds semantic literal types corresponding to the syntactic literals in the interest of consistency and on the grounds that if a type is important enough to warrant first class syntax it is important enough to warrant first class singleton types.

    Note that shapeless in current Scala provides an encoding of singleton types for Symbol as the type Symbol tagged with the literal type of its corresponding String.

    Example,

    valueOf['foo]                      // result is 'foo: 'foo
    

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.

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

As discussed in the proposal above, an important motivation for including first class literal types for Scala Symbol literals is that they have first class syntax – if something is important enough to warrant syntax then it should be important enough to warrant a corresponding literal type.

The converse also holds, and here we have two notable missing cases: Byte and Short. These 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.

  • 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)
}