@@ -33,17 +33,17 @@ their role is to give the meaning of paths selecting types and terms from nested
3333paths have an intuitive meaning to programmers from a wide range of backgrounds which belies their
3434underpinning by a somewhat "advanced" concept in type theory.
3535
36- Nevertheless, by pairing a type with it's unique inhabitant, singleton types bridge the gap between
37- types and values, and their presence in Scala has over the years allowed Scala programmers to explore
38- techniques which would typically only be available in languages, such as Agda or Idris, with support
36+ Nevertheless, by pairing a type with its unique inhabitant, singleton types bridge the gap between
37+ types and values, and their presence in Scala has, over the years, allowed Scala programmers to explore
38+ techniques which would typically only be available in languages such as Agda or Idris, with support
3939for full-spectrum dependent types.
4040
4141Scala's semantics have up until now been richer than its syntax. The only singleton types which are
4242currently _ directly_ expressible are those of the form ` p.type ` where ` p ` is a path pointing to a
4343value of some subtype of ` AnyRef ` . Internally the Scala compiler also represents singleton types for
44- individual values of subtypes of ` AnyVal ` , such as ` Int ` or values of type ` String ` which don't
44+ individual values of subtypes of ` AnyVal ` , such as ` Int ` or values of type ` String ` , which don't
4545correspond to paths. These types are inferred in some circumstances, notably as the types of ` final `
46- vals. Their primary purpose has been to represent compile time constants (see [ 6.24 Constant
46+ vals. Their primary purpose has been to represent compile- time constants (see [ 6.24 Constant
4747Expressions] ( https://scala-lang.org/files/archive/spec/2.12/06-expressions.html#constant-expressions )
4848and the discussion of "constant value definitions" in [ 4.1 Value Declarations and
4949Definitions] ( https://scala-lang.org/files/archive/spec/2.12/04-basic-declarations-and-definitions.html#value-declarations-and-definitions ) ).
@@ -89,15 +89,15 @@ Lightbend Scala compiler.
8989 foo(1: 1) // type ascription
9090 ```
9191
92- + The ` .type ` singleton type forming operator can be applied to values of all subtypes of ` Any ` .
93- To prevent the compiler from widening our return type we assign to a final val.
92+ + The ` .type ` singleton- type- forming operator can be applied to values of all subtypes of ` Any ` .
93+ To prevent the compiler from widening our return type, we assign to a final val.
9494 ```
9595 def foo[T](t: T): t.type = t
9696 final val bar = foo(23) // result is bar: 23
9797 ```
9898
9999+ The presence of an upper bound of ` Singleton ` on a formal type parameter indicates that
100- singleton types should be inferred for type parameters at call sites. To help see this
100+ singleton types should be inferred for type parameters at call sites. To help see this,
101101 we introduce type constructor ` Id ` to prevent the compiler from widening our return type.
102102 ```
103103 type Id[A] = A
@@ -118,7 +118,7 @@ Lightbend Scala compiler.
118118 ```
119119
120120+ A ` scala.ValueOf[T] ` type class and corresponding ` scala.Predef.valueOf[T] ` operator has been
121- added yielding the unique value of types with a single inhabitant.
121+ added, yielding the unique value of types with a single inhabitant.
122122 ```
123123 def foo[T](implicit v: ValueOf[T]): T = v.value
124124 foo[13] // result is 13: Int
@@ -129,13 +129,13 @@ Lightbend Scala compiler.
129129
130130Many of the examples below use primitives provided by the Scala generic programming library
131131[ shapeless] ( https://github.com/milessabin/shapeless/ ) . It provides a ` Witness ` type class and a
132- family of Scala macro based methods and conversions for working with singleton types and shifting
132+ family of Scala- macro- based methods and conversions for working with singleton types and shifting
133133from the value to the type level and vice versa. One of the goals of this SIP is to enable Scala
134134programmers to achieve similar results without having to rely on a third party library or fragile
135135and non-portable macros.
136136
137137The relevant parts of shapeless are excerpted in [ Appendix 1] ( #appendix-1--shapeless-excerpts ) .
138- Given the definitions there, some of forms summarized above can be expressed in current Scala,
138+ Given the definitions there, some of the forms summarized above can be expressed in current Scala,
139139```
140140val wOne = Witness(1)
141141val one: wOne.T = wOne.value // wOne.T is the type 1
@@ -147,13 +147,13 @@ foo[wOne.T] // result is 1: 1
147147"foo" ->> 23 // shapeless record field constructor
148148 // result type is FieldType["foo", Int]
149149```
150- The syntax is awkward and hiding it from library users is challenging. Nevertheless they enable many
150+ The syntax is awkward, and hiding it from library users is challenging. Nevertheless they enable many
151151constructs which have proven valuable in practice.
152152
153153#### shapeless records
154154
155155shapeless models records as HLists (essentially nested pairs) of record values with their types
156- tagged with the singleton types of their keys. The library provides user friendly mechanisms for
156+ tagged with the singleton types of their keys. The library provides user- friendly mechanisms for
157157constructing record _ values_ , however it is extremely laborious to express the corresponding _ types_ .
158158Consider the following record value,
159159```
@@ -165,7 +165,7 @@ val book =
165165 HNil
166166```
167167
168- Using shapeless and current Scala the following would be required to give ` book ` an explicit type
168+ Using shapeless and current Scala, the following would be required to give ` book ` an explicit type
169169annotation,
170170```
171171val wAuthor = Witness("author")
@@ -241,20 +241,20 @@ val c: Int Refined Greater[w6.T] = a
241241 ^
242242```
243243
244- Under this proposal we can express these refinements much more succinctly,
244+ Under this proposal, we can express these refinements much more succinctly,
245245```
246246val a: Int Refined Greater[5] = 10
247247
248248val b: Int Refined Greater[4] = a
249249```
250250
251- Type level predicates of this kind have proved to be useful in practice and are supported by modules
251+ Type- level predicates of this kind have proved to be useful in practice and are supported by modules
252252of a [ number of important libraries] ( https://github.com/fthomas/refined#external-modules ) .
253253
254254Experience with those libraries has led to a desire to compute directly over singleton types, in
255- effect to lift whole term-level expressions to the type- level which has resulted in the development
255+ effect to lift whole term-level expressions to the type level, which has resulted in the development
256256of the [ singleton-ops] ( https://github.com/fthomas/singleton-ops ) library. singleton-ops is built
257- with Typelevel Scala which allows it to use literal types as discussed in this SIP.
257+ with Typelevel Scala, which allows it to use literal types, as discussed in this SIP.
258258
259259```
260260import singleton.ops._
@@ -279,7 +279,7 @@ singleton-ops is used by a number of libraries, most notably our next motivating
279279
280280[ Libra] ( https://github.com/to-ithaca/libra ) is a a dimensional analysis library based on shapeless,
281281spire and singleton-ops. It support SI units at the type level for all numeric types. Like
282- singleton-ops Libra is built using Typelevel Scala and so is able to use literal types as discussed
282+ singleton-ops, Libra is built using Typelevel Scala and so is able to use literal types, as discussed
283283in this SIP.
284284
285285Libra allows numeric computations to be checked for dimensional correctness as follows,
@@ -324,7 +324,7 @@ case class Residue[M <: Int](n: Int) extends AnyVal {
324324}
325325```
326326
327- Given this definition we can work with modular numbers without any danger of mixing numbers with
327+ Given this definition, we can work with modular numbers without any danger of mixing numbers with
328328different moduli,
329329
330330```
@@ -342,7 +342,7 @@ fiveModTen + fourModEleven
342342```
343343
344344Also note that the use of ` ValueOf ` as an implicit argument of ` + ` means that the modulus does not
345- need to be stored along with the ` Int ` in the ` Residue ` value which could be beneficial in
345+ need to be stored along with the ` Int ` in the ` Residue ` value, which could be beneficial in
346346applications which work with large datasets.
347347
348348### Proposal details
@@ -360,15 +360,15 @@ applications which work with large datasets.
360360 | ‘(’ Types ‘)’
361361 ```
362362
363- Examples,
363+ Examples:
364364 ```
365365 val one: 1 = 1 // val declaration
366366 def foo(x: 1): Option[1] = Some(x) // param type, type arg
367367 def bar[T <: 1](t: T): T = t // type parameter bound
368368 foo(1: 1) // type ascription
369369 ```
370370
371- + The restriction that the singleton type forming operator ` .type ` can only be appended to
371+ + The restriction that the singleton- type- forming operator ` .type ` can only be appended to
372372 stable paths designating a value which conforms to ` AnyRef ` is dropped -- the path may now conform
373373 to ` Any ` . Section
374374 [ 3.2.1] ( https://scala-lang.org/files/archive/spec/2.12/03-types.html#singleton-types ) of the SLS is
@@ -385,7 +385,7 @@ applications which work with large datasets.
385385 > denoted by `p` (i.e., the value `v` for which `v eq p`). Where the path does not conform to
386386 > `scala.AnyRef` the type denotes the set consisting of only the value denoted by `p`.
387387
388- Example,
388+ Example:
389389 ```
390390 def foo[ T] (t: T): t.type = t
391391 final val bar = foo(23) // result is bar: 23
@@ -471,7 +471,7 @@ applications which work with large datasets.
471471 > corresponding to a singleton-apt definition, or (2) The upper bound Ui of Ti conforms to
472472 > `Singleton`.
473473
474- Example,
474+ Example:
475475 ```
476476 type Id[ A] = A
477477 def wide[ T] (t: T): Id[ T] = t
@@ -483,17 +483,17 @@ applications which work with large datasets.
483483 Note that we introduce the type constructor `Id` simply to avoid widening of the return type.
484484
485485+ A `scala.ValueOf[T]` type class and corresponding `scala.Predef.valueOf[T]` operator has been
486- added yielding the unique value of types with a single inhabitant.
486+ added, yielding the unique value of types with a single inhabitant.
487487
488488 Type inference allows us to infer a singleton type from a literal value. It is natural to want to
489489 be able to go in the other direction and infer a value from a singleton type. This latter
490490 capability was exploited in the motivating `Residue` example given earlier, and is widely relied
491- on in current Scala in uses of shapeless's records, and `LabelledGeneric` based type class
491+ on in current Scala in uses of shapeless's records, and `LabelledGeneric`- based type class
492492 derivation.
493493
494- Implicit resolution is Scala's mechanism for inferring values from types and in current Scala
494+ Implicit resolution is Scala's mechanism for inferring values from types, and in current Scala,
495495 shapeless provides a macro-based materializer for instances of its `Witness` type class. This SIP
496- adds a directly compiler supported type class as a replacement,
496+ adds a directly compiler- supported type class as a replacement:
497497
498498 ```
499499 final class ValueOf[ T] (val value: T) extends AnyVal
@@ -502,20 +502,20 @@ applications which work with large datasets.
502502 Instances are automatically provided for all types with a single inhabitant, which includes
503503 literal and non-literal singleton types and `Unit`.
504504
505- Example,
505+ Example:
506506 ```
507507 def foo[ T] (implicit v: ValueOf[ T] ): T = v.value
508508 foo[ 13] // result is 13: Int
509509 ```
510510
511- A method `valueOf` is also added to `scala.Predef` analogously to existing operators such as
511+ A method `valueOf` is also added to `scala.Predef`, analogously to existing operators such as
512512 `classOf`, `typeOf` etc.
513513
514514 ```
515515 def valueOf[ T] (implicit vt: ValueOf[ T] ): T = vt.value
516516 ```
517517
518- Example,
518+ Example:
519519 ```
520520 object Foo
521521 valueOf[ Foo.type] // result is Foo: Foo.type
@@ -531,11 +531,11 @@ applications which work with large datasets.
531531 where the `TypePat` is a literal type is translated as a match against the subsuming non-singleton
532532 type followed by an equality test with the value corresponding to the literal type.
533533
534- Where applied to literal types `isInstanceOf` is translated to a test against
534+ Where applied to literal types, `isInstanceOf` is translated to a test against
535535 the subsuming non-singleton type and an equality test with the value corresponding to the literal
536536 type.
537537
538- Examples,
538+ Examples:
539539 ```
540540 (1: Any) match {
541541 case one: 1 => true
@@ -544,36 +544,36 @@ applications which work with large datasets.
544544 (1: Any).isInstanceOf[ 1] // result is true: Boolean
545545 ```
546546
547- Importantly, that doesn't include `asInstanceOf` as that is a user assertion to the compiler, with
547+ Importantly, that doesn't include `asInstanceOf`, as that is a user assertion to the compiler, with
548548 the compiler inserting in the generated code just enough code for the underlying runtime to not
549549 give a `ValidationError`. The compiler should not, for instance, generate code such that an
550550 expression like `(1: Any).asInstanceOf[2]` would throw a `ClassCastException`.
551551
552552+ Default initialization for vars with literal types is forbidden.
553553
554- The default initializer for a var is already mandated to be it's natural zero element (`0`,
555- `false`, `null` etc.). This is inconsistent with the var being given a non-zero literal type,
554+ The default initializer for a var is already mandated to be its natural zero element (`0`,
555+ `false`, `null` etc.). This is inconsistent with the var being given a non-zero literal type:
556556
557557 ```
558558 var bad: 1 = _
559559 ```
560- Whilst we could, in principle, provide an implicit non-default initializer for cases such as these
560+ Whilst we could, in principle, provide an implicit non-default initializer for cases such as these,
561561 it is the view of the authors of this SIP that there is nothing to be gained from enabling this
562- construction and that default initializer should be forbidden.
562+ construction, and that default initializer should be forbidden.
563563
564564
565- ## Follow on work from this SIP
565+ ## Follow- on work from this SIP
566566
567567Whilst the authors of this SIP believe that it stands on its own merits, we think that there are two
568- areas where follow on work is desirable, and one area where another SIP might improve the implementation of SIP-23.
568+ areas where follow- on work is desirable, and one area where another SIP might improve the implementation of SIP-23.
569569
570570### Infix and prefix types
571571
572572[SIP-33 Match Infix and Prefix Types to Meet Expression Rules](https://docs.scala-lang.org/sips/priority-based-infix-type-precedence.html)
573573has emerged from the work on refined types and computation over singleton types mentioned in the
574574motivation section above.
575575
576- Once literal types are available it is natural to want to lift entire expressions to the type level
576+ Once literal types are available, it is natural to want to lift entire expressions to the type level
577577as is done already in libraries such as [singleton-ops](https://github.com/fthomas/singleton-ops).
578578However, the precedence and associativity of symbolic infix _type constructors_ don't match the
579579precedence and associativity of symbolic infix _value operators_, and prefix type constructors don't
@@ -583,12 +583,12 @@ terms.
583583### Byte and short literals
584584
585585`Byte` and `Short` have singleton types, but lack any corresponding syntax either at the type or at the term level.
586- These types are important in libraries which deal with low level numerics and protocol implementation
586+ These types are important in libraries which deal with low- level numerics and protocol implementation
587587(see eg. [Spire](https://github.com/non/spire) and [Scodec](https://github.com/scodec/scodec)) and
588588elsewhere, and the ability to, for instance, index a type class by a byte or short literal would be
589589valuable.
590590
591- A prototype of this syntax extension existed at an early stage in the development of Typelevel Scala
591+ A prototype of this syntax extension existed at an early stage in the development of Typelevel Scala,
592592but never matured. The possibility of useful literal types adds impetus.
593593
594594### Opaque types
@@ -610,7 +610,7 @@ would be elided, and the `valueOf[A]` method would be compiled to an identity fu
610610
611611## Appendix 1 -- shapeless excerpts
612612
613- Extracts from shapeless relevant to the motivating examples for this SIP,
613+ Extracts from shapeless relevant to the motivating examples for this SIP:
614614
615615```
616616trait Witness {
0 commit comments