Dotty: The Singleton "kind" is not an upper bound

[Blaisorblade]

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]

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

[milessabin]

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.

[soronpo]

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 https://github.com/scala/bug/issues/10838

[odersky]

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?

[milessabin]

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.

[milessabin]

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.

[odersky]

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.

[milessabin]

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 = ...

[milessabin]

Or, for that matter,

def f(implicit u: Universe)(m: Mirror[u.type]): u.Tree = ...

[odersky]

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?

[milessabin]

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?

[odersky]

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.

[Blaisorblade]

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.

[joshlemer]

Created at topic of discussion here

[nafg]

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

[Blaisorblade]

@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]

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 [e-mail]
wrote:

@nafg https://github.com/nafg Interesting idea!
Take def gU <: Universe with Singleton = ....
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 https://github.com/lampepfl/dotty/pull/5458) syntax:

def gU <: Universe with Singleton(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
https://github.com/lampepfl/dotty/pull/5825).

—
You are receiving this because you were mentioned.
Reply to this email directly, view it on GitHub
https://github.com/lampepfl/dotty/issues/4944#issuecomment-459592170,
or mute the thread
https://github.com/notifications/unsubscribe-auth/AAGAUE0EGtIqlteu-PwJJ9QEgW-l50f8ks5vI7NcgaJpZM4V8-EJ
.

[milessabin]

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.

[LPTK]

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.

[odersky]

@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?

[odersky]

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

[joshlemer]

@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

[LPTK]

@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.