# The Singleton "kind" is not an upper bound #4944

Open
opened this Issue Aug 14, 2018 · 23 comments

Projects
None yet
7 participants
Contributor

### Blaisorblade commented Aug 14, 2018

 A few of us discussed this, but it seems we lack an issue for it. Quoting from #4942: If A <: Singleton and B <: Singleton, it follows that A | B <: Singleton, but for instance 1 | 2 is not actually a singleton type. In fact, already in Scala 2 we can exploit this and write the questionable ``` def f[Bound, A <: Bound, B <: Bound](cond: Boolean, a: A, b: B): Bound = if (cond) a else b def g(cond: Boolean): Singleton = f[Singleton, 1, 2](cond, 1, 2)``` In Dotty we also get the clearly broken: ``` def f[Bound, A <: Bound, B <: Bound](cond: Boolean, a: A, b: B): (A | B) & Bound = if (cond) a else b def g(cond: Boolean): Singleton = f[Singleton, 1, 2](cond, 1, 2) // def h(cond: Boolean): (1|2) & Singleton = f[Singleton, 1, 2](cond, 1, 2) // doesn't compile type || [A, B] = A | B type Boo = 0 || 1 // def h1(cond: Boolean): (1||2) & Singleton = f[Singleton, 1, 2](cond, 1, 2) // still fails because 1 | 2 is collapsed eagerly def f2[Bound, A <: Bound, B <: Bound](cond: Boolean, a: A, b: B): (A || B) & Bound = if (cond) a else b def h2(cond: Boolean): (1||2) & Singleton = f2[Singleton, 1, 2](cond, 1, 2) def h2(cond: Boolean): Int(1) Any Int(2) & Singleton``` Only `h` fails, and just because we forbid `1|2` syntactically for now (#1551), so `h2` works. Since `Singleton` is special in core typing rules, @odersky suggested this endangers even soundness. Ad-hoc restrictions (say, forbidding `Singleton` as a type argument) seems a losing whack-a-mole game. Discussing this with @odersky today, we figured that `Singleton` behaves like a kind that can't be expressed via upper bounds, so we should consider something like an annotation or a modifier (tho modifiers on type variables don't exist yet). Migration isn't easy, but one can easily support simple use cases of form `[X <: Singleton]` or even `[X <: Foo with Singleton]`. According to @nicolasstucki, even `type SingAlias = Singleton; def foo[X <: Foo with SingAlias]` doesn't currently work. Paging @milessabin and @soronpo, as this affects SIP-23.

### Blaisorblade added itype:bug area:typer prio:high stat:needs spec labels Aug 14, 2018

Contributor Author

### Blaisorblade commented Aug 14, 2018

 Marked with `prio:high` because @odersky said this is used relatively often.
Contributor

### milessabin commented Aug 14, 2018

 The use of `Singleton` bounds in SIP 23 and elsewhere in Scala 2 is almost entirely to influence type inference rather than to express a meaningful subtype relationship. I'd be open to there being an alternative mechanism for doing that.
Contributor

### soronpo commented Aug 14, 2018

 The use of Singleton bounds in SIP 23 and elsewhere in Scala 2 is almost entirely to influence type inference rather than to express a meaningful subtype relationship. I'd be open to there being an alternative mechanism for doing that. And while we're at it, perhaps find a way to solve scala/bug#10838
Contributor

### odersky commented Aug 14, 2018 • edited

 The use of Singleton bounds in SIP 23 and elsewhere in Scala 2 is almost entirely to influence type inference rather than to express a meaningful subtype relationship. Yes, that seems to be the case. I believe the only necessary use case of `Singleton` is to signal "don't widen this type argument". Expressing this with a subtype relationship is wrong. We need a label/modifier on the type parameter instead. Something like ``````def f[singleton T] `````` It would mean complicating the syntax by allowing a modifier on type parameters. Does anybody see an alternative way to express this?
Contributor

### milessabin commented Aug 14, 2018

 Does anybody see an alternative way to express this? We have at least two areas where we want to be able to influence inference: type inference, as here (I suspect that there will more cases than just "don't widen" to be found if we go looking); and also term inference, as in implicit search. My hunch is that it would be worth exploring the idea of a something like a tactic language to deal with both of these.
Contributor

### milessabin commented Aug 15, 2018

 A few examples in addition to inferring a singleton type if possible, Infer a concrete subtype of an ADT or infer the super type? Infer `Nothing` or not? Infer `Any` or not? Infer `Product with Serializable` or not? I'm sure there are plenty more ... In all these cases we can pick a most likely option, but there will be a significant number of scenarios where the most likely option isn't the right one. Parenthetically, we need to be careful not to throw the baby out with the bath water ... there are cases where we want to accept only singleton typed terms, ie. where we want to ensure we have a stable value.
Contributor

### odersky commented Aug 15, 2018

 Parenthetically, we need to be careful not to throw the baby out with the bath water ... there are cases where we want to accept only singleton typed terms, ie. where we want to ensure we have a stable value. Indeed. Right now, a typical pattern would be like this: `def f[U <: Universe with Singleton](m: Mirror[U]): U#Tree = ...` The "only singleton type" guarantee is important to ensure that `U#Tree` is well-formed. What we are trying to do here is pass a path as an argument, but as a type, not as a term. Maybe we can express this more directly? `def f[u.type <: Universe](m: Mirror[u.type]): u.Tree` The scheme would be to have a limited form of type pattern in type parameter binding position. A type pattern is either a type name or a term name followed by `.type`. In the second case, i.e. ``````x.type <: A `````` the term name `x` introduces an `erased` value of type `A`. This means no actual argument needs to be passed and `x` can be used only as a type prefix, never as a term prefix.
Contributor

### milessabin commented Aug 15, 2018 • edited

 I think that's a good example of how type and term inference are related. Couldn't we have something like, `def f(m: Mirror[u.type])(implicit u: Universe): u.Tree = ...`
Contributor

### milessabin commented Aug 15, 2018

 Or, for that matter, `def f(implicit u: Universe)(m: Mirror[u.type]): u.Tree = ...`
Contributor

### odersky commented Aug 15, 2018 • edited

 We can't have this, since `u` is used before being defined, and I fear that would be hard to change. `def f(m: Mirror[u.type])(implicit u: Universe): u.Tree = ...` But we could have the second version: `def f(implicit erased u: Universe)(m: Mirror[u.type]) u.Tree = ...` It's not completely equivalent, since it does not allow us to infer `u` from `m`, but that looks like a minor inconvenience. So maybe the answer is: just deprecate `Singleton` instead of trying to fix it?
Contributor

### milessabin commented Aug 15, 2018

 It's not completely equivalent, since it does not allow us to infer u from m This is something that's been bugging me for some time now. Why is it possible that in this case, `def foo[Eariler](later: Foo[Earlier]) ...` we can infer the `Earlier` from `later`, whereas in this case, `def foo(implicit earlier: Whatever)(later: Foo[earlier.type]) ...` we can't infer `earlier` from `later`?
Contributor

### odersky commented Aug 15, 2018 • edited

 we can't infer earlier from later? This would mean implicit search and local type inference are merged into one. I fear that would make implicit search a lot more complex and less predictable. Also, in the example we are discussing the `implicit` it actually misleading. We'd be perfectly happy with a non-implicit universe that's determined by a mirror.
Contributor Author

### Blaisorblade commented Aug 15, 2018

 The "only singleton type" guarantee is important to ensure that U#Tree is well-formed. What we are trying to do here is pass a path as an argument, but as a type, not as a term. Do we really need singletons, or just realizable types there? But I think there are scenarios where Singleton is necessary as-is, for instance for singleton-ops. @milessabin Indeed, in Agda there are separate mechanisms for unification-based inference (Agda implicit arguments, or Scala type arguments) and instance-based inference (Agda instance arguments, or Scala implicit arguments). The search semantics are different, but whether something is a term or a type doesn’t matter at all. But that’s not easy to retrofit, and Scala replaces unification with subtyping, which isn’t obvious on the term level. Meanwhile, in Scala I suspect default arguments given by transparent functions would enable programmable inference tactics and be easier to achieve.

Closed

### joshlemer commented Jan 31, 2019

 Created at topic of discussion here

### nafg commented Jan 31, 2019

 Why can't it be done with a special typeclass?
Contributor Author

### Blaisorblade commented Feb 1, 2019

 @nafg Interesting idea! Take `def g[U <: Universe with Singleton](m: Mirror[U], x: U#Tree) = ...`. We probably need the typeclass instance in scope where `U#Tree` appears, so it must be an earlier argument — which the new implicits allow. In old and "new" (#5458) syntax: ```def g[U <: Universe with Singleton](implicit us: IsSingleton[U])(m: Mirror[U], x: U#Tree) = ... def g[U <: Universe with Singleton] with IsSingleton[U] (m: Mirror[U], x: U#Tree) = ...``` (Beware the new syntax is still in flux, per #5825).

### nafg commented Feb 1, 2019

 BTW it seems Martin suggested it on the forum thread before I posted it here. … On Thu, Jan 31, 2019, 10:24 PM Paolo G. Giarrusso ***@***.***> wrote: @nafg Interesting idea! Take def g[U <: Universe with Singleton](m: Mirror[U], x: U#Tree) = .... We probably need the typeclass instance in scope where U#Tree appears, so it must be an earlier argument — which the new implicits allow. In old and "new" (#5458 <#5458>) syntax: def g[U <: Universe with Singleton](implicit us: IsSingleton[U])(m: Mirror[U], x: U#Tree) = ... def g[U <: Universe with Singleton] with IsSingleton[U] (m: Mirror[U], x: U#Tree) = ... (Beware the new syntax is still in flux, per #5825 <#5825>). — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#4944 (comment)>, or mute the thread .
Contributor

### milessabin commented Feb 1, 2019

 I don't think a special type class is the way to go. The problem that the `<: Singleton` bound solves (badly) is affecting type inference by preventing widening. A type class constraint doesn't help with that without an awful lot of special-casing. See my comments on the contributors thread here.
Contributor

### LPTK commented Feb 1, 2019 • edited

 Here is how a singleton type bound could work: The `Singleton` type is parameterized and contravariant: `type Singleton[-T]` Users write bounds as `T <: Singleton[T]`, which could also be syntax-sugared with an annotation: ```class C[A <: Singleton[A]](a: A) // or with sugar: class C[@singleton A](a: A)``` The type of every value `v` extends `Singleton[v.type]`. Non-singleton types naturally could extend `Singleton[Nothing]`, which would be like a top type, but it's not really useful as we already have `Any`. In any case we do have `v.type | w.type <: Singleton[v.type] | Singleton[w.type] =:= Singleton[v.type & w.type] <: Singleton[Nothing]`. In the example above, you can't instantiate `C` with a non-singleton type, because that would mean having to pass an `a` argument typed `Nothing` or some other impossible stuff (like `v.type & w.type`). The compiler could then provide useful reasoning on such types, such as `List[Int] & Singleton[x.type] <: x.type`. This would actually be useful to reason modularly about subtyping knowledge involving singleton types, which is currently very hard – sometimes we want to refine a singleton type with a type that is more precise than its widened form.
Contributor

### odersky commented Feb 1, 2019 • edited

 @LPTK Interesting! So we only need the subtype checker to implement ``````P <:< Singleton[P] `````` for any singleton type `P`, and keep the widen restriction on instantiation, and everything else falls out?
Contributor

### odersky commented Feb 1, 2019

 Can someone remind me whether Scala 2 supports `Singleton`? In that case we'd need a new name for the F-bounded version.

### joshlemer commented Feb 1, 2019

 @odersky yes `Singleton` exists at least as far back as 2.11 ``````Welcome to Scala 2.11.11 (Java HotSpot(TM) 64-Bit Server VM, Java 1.8.0_151). Type in expressions for evaluation. Or try :help. scala> val s: Singleton = List s: Singleton = scala.collection.immutable.List\$@ab6cf07 ``````
Contributor

### LPTK commented Feb 1, 2019

 @odersky So we only need the subtype checker to implement `P <:< Singleton[P]` for any singleton type `P`, and keep the widen restriction on instantiation, and everything else falls out? I believe so, yes. `Singleton` would have to be deprecated, and maybe we can add `Singleton[S]` to a language import? As in `import scala.language.Singleton`.