@@ -33,17 +33,17 @@ their role is to give the meaning of paths selecting types and terms from nested
33
33
paths have an intuitive meaning to programmers from a wide range of backgrounds which belies their
34
34
underpinning by a somewhat "advanced" concept in type theory.
35
35
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
39
39
for full-spectrum dependent types.
40
40
41
41
Scala's semantics have up until now been richer than its syntax. The only singleton types which are
42
42
currently _ directly_ expressible are those of the form ` p.type ` where ` p ` is a path pointing to a
43
43
value 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
45
45
correspond 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
47
47
Expressions] ( https://scala-lang.org/files/archive/spec/2.12/06-expressions.html#constant-expressions )
48
48
and the discussion of "constant value definitions" in [ 4.1 Value Declarations and
49
49
Definitions] ( 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.
89
89
foo(1: 1) // type ascription
90
90
```
91
91
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.
94
94
```
95
95
def foo[T](t: T): t.type = t
96
96
final val bar = foo(23) // result is bar: 23
97
97
```
98
98
99
99
+ 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,
101
101
we introduce type constructor ` Id ` to prevent the compiler from widening our return type.
102
102
```
103
103
type Id[A] = A
@@ -118,7 +118,7 @@ Lightbend Scala compiler.
118
118
```
119
119
120
120
+ 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.
122
122
```
123
123
def foo[T](implicit v: ValueOf[T]): T = v.value
124
124
foo[13] // result is 13: Int
@@ -129,13 +129,13 @@ Lightbend Scala compiler.
129
129
130
130
Many of the examples below use primitives provided by the Scala generic programming library
131
131
[ 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
133
133
from the value to the type level and vice versa. One of the goals of this SIP is to enable Scala
134
134
programmers to achieve similar results without having to rely on a third party library or fragile
135
135
and non-portable macros.
136
136
137
137
The 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,
139
139
```
140
140
val wOne = Witness(1)
141
141
val one: wOne.T = wOne.value // wOne.T is the type 1
@@ -147,13 +147,13 @@ foo[wOne.T] // result is 1: 1
147
147
"foo" ->> 23 // shapeless record field constructor
148
148
// result type is FieldType["foo", Int]
149
149
```
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
151
151
constructs which have proven valuable in practice.
152
152
153
153
#### shapeless records
154
154
155
155
shapeless 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
157
157
constructing record _ values_ , however it is extremely laborious to express the corresponding _ types_ .
158
158
Consider the following record value,
159
159
```
@@ -165,7 +165,7 @@ val book =
165
165
HNil
166
166
```
167
167
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
169
169
annotation,
170
170
```
171
171
val wAuthor = Witness("author")
@@ -241,20 +241,20 @@ val c: Int Refined Greater[w6.T] = a
241
241
^
242
242
```
243
243
244
- Under this proposal we can express these refinements much more succinctly,
244
+ Under this proposal, we can express these refinements much more succinctly,
245
245
```
246
246
val a: Int Refined Greater[5] = 10
247
247
248
248
val b: Int Refined Greater[4] = a
249
249
```
250
250
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
252
252
of a [ number of important libraries] ( https://github.com/fthomas/refined#external-modules ) .
253
253
254
254
Experience 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
256
256
of 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.
258
258
259
259
```
260
260
import singleton.ops._
@@ -279,7 +279,7 @@ singleton-ops is used by a number of libraries, most notably our next motivating
279
279
280
280
[ Libra] ( https://github.com/to-ithaca/libra ) is a a dimensional analysis library based on shapeless,
281
281
spire 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
283
283
in this SIP.
284
284
285
285
Libra allows numeric computations to be checked for dimensional correctness as follows,
@@ -324,7 +324,7 @@ case class Residue[M <: Int](n: Int) extends AnyVal {
324
324
}
325
325
```
326
326
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
328
328
different moduli,
329
329
330
330
```
@@ -342,7 +342,7 @@ fiveModTen + fourModEleven
342
342
```
343
343
344
344
Also 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
346
346
applications which work with large datasets.
347
347
348
348
### Proposal details
@@ -360,15 +360,15 @@ applications which work with large datasets.
360
360
| ‘(’ Types ‘)’
361
361
```
362
362
363
- Examples,
363
+ Examples:
364
364
```
365
365
val one: 1 = 1 // val declaration
366
366
def foo(x: 1): Option[1] = Some(x) // param type, type arg
367
367
def bar[T <: 1](t: T): T = t // type parameter bound
368
368
foo(1: 1) // type ascription
369
369
```
370
370
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
372
372
stable paths designating a value which conforms to ` AnyRef ` is dropped -- the path may now conform
373
373
to ` Any ` . Section
374
374
[ 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.
385
385
> denoted by `p` (i.e., the value `v` for which `v eq p`). Where the path does not conform to
386
386
> `scala.AnyRef` the type denotes the set consisting of only the value denoted by `p`.
387
387
388
- Example,
388
+ Example:
389
389
```
390
390
def foo[ T] (t: T): t.type = t
391
391
final val bar = foo(23) // result is bar: 23
@@ -471,7 +471,7 @@ applications which work with large datasets.
471
471
> corresponding to a singleton-apt definition, or (2) The upper bound Ui of Ti conforms to
472
472
> `Singleton`.
473
473
474
- Example,
474
+ Example:
475
475
```
476
476
type Id[ A] = A
477
477
def wide[ T] (t: T): Id[ T] = t
@@ -483,17 +483,17 @@ applications which work with large datasets.
483
483
Note that we introduce the type constructor `Id` simply to avoid widening of the return type.
484
484
485
485
+ 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.
487
487
488
488
Type inference allows us to infer a singleton type from a literal value. It is natural to want to
489
489
be able to go in the other direction and infer a value from a singleton type. This latter
490
490
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
492
492
derivation.
493
493
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,
495
495
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:
497
497
498
498
```
499
499
final class ValueOf[ T] (val value: T) extends AnyVal
@@ -502,20 +502,20 @@ applications which work with large datasets.
502
502
Instances are automatically provided for all types with a single inhabitant, which includes
503
503
literal and non-literal singleton types and `Unit`.
504
504
505
- Example,
505
+ Example:
506
506
```
507
507
def foo[ T] (implicit v: ValueOf[ T] ): T = v.value
508
508
foo[ 13] // result is 13: Int
509
509
```
510
510
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
512
512
`classOf`, `typeOf` etc.
513
513
514
514
```
515
515
def valueOf[ T] (implicit vt: ValueOf[ T] ): T = vt.value
516
516
```
517
517
518
- Example,
518
+ Example:
519
519
```
520
520
object Foo
521
521
valueOf[ Foo.type] // result is Foo: Foo.type
@@ -531,11 +531,11 @@ applications which work with large datasets.
531
531
where the `TypePat` is a literal type is translated as a match against the subsuming non-singleton
532
532
type followed by an equality test with the value corresponding to the literal type.
533
533
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
535
535
the subsuming non-singleton type and an equality test with the value corresponding to the literal
536
536
type.
537
537
538
- Examples,
538
+ Examples:
539
539
```
540
540
(1: Any) match {
541
541
case one: 1 => true
@@ -544,36 +544,36 @@ applications which work with large datasets.
544
544
(1: Any).isInstanceOf[ 1] // result is true: Boolean
545
545
```
546
546
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
548
548
the compiler inserting in the generated code just enough code for the underlying runtime to not
549
549
give a `ValidationError`. The compiler should not, for instance, generate code such that an
550
550
expression like `(1: Any).asInstanceOf[2]` would throw a `ClassCastException`.
551
551
552
552
+ Default initialization for vars with literal types is forbidden.
553
553
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:
556
556
557
557
```
558
558
var bad: 1 = _
559
559
```
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,
561
561
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.
563
563
564
564
565
- ## Follow on work from this SIP
565
+ ## Follow- on work from this SIP
566
566
567
567
Whilst 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.
569
569
570
570
### Infix and prefix types
571
571
572
572
[SIP-33 Match Infix and Prefix Types to Meet Expression Rules](https://docs.scala-lang.org/sips/priority-based-infix-type-precedence.html)
573
573
has emerged from the work on refined types and computation over singleton types mentioned in the
574
574
motivation section above.
575
575
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
577
577
as is done already in libraries such as [singleton-ops](https://github.com/fthomas/singleton-ops).
578
578
However, the precedence and associativity of symbolic infix _type constructors_ don't match the
579
579
precedence and associativity of symbolic infix _value operators_, and prefix type constructors don't
@@ -583,12 +583,12 @@ terms.
583
583
### Byte and short literals
584
584
585
585
`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
587
587
(see eg. [Spire](https://github.com/non/spire) and [Scodec](https://github.com/scodec/scodec)) and
588
588
elsewhere, and the ability to, for instance, index a type class by a byte or short literal would be
589
589
valuable.
590
590
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,
592
592
but never matured. The possibility of useful literal types adds impetus.
593
593
594
594
### Opaque types
@@ -610,7 +610,7 @@ would be elided, and the `valueOf[A]` method would be compiled to an identity fu
610
610
611
611
## Appendix 1 -- shapeless excerpts
612
612
613
- Extracts from shapeless relevant to the motivating examples for this SIP,
613
+ Extracts from shapeless relevant to the motivating examples for this SIP:
614
614
615
615
```
616
616
trait Witness {
0 commit comments