A uniform and compact syntax for singleton types

Language Design
1

I’d like to get some opinions on an alternative syntax for singleton types.

Status quo

At the moment we have a different syntax to describe literals and stable paths:

val c: 1 = 1
val z: x.y.type = x.y

though the distinction strikes me as a bit arbitrary. Furthermore, the common case of a path dependency on some parameter is rather verbose (e.g. x.type).

Proposal

I would like to propose an alternative syntax for singleton types that is both uniform and concise: If we parse a type T of the form '{' expr '}' and the type of expr before widening is stable, then T may be used as a singleton type.

For instance, the above example would become more consistent and (arguably) slightly more legible:

val c: {1} = 1
val z: {x.y} = x.y

Besides the uniformity I like this syntax for having intuitive semantics: as types, {1} and {x.y} correspond to the singleton sets of their underlying expressions, 1 and x.y.

My original motivation was to come up with an alternative syntax that’s also pleasant when dealing with more complex singletons. In a recent Dotty PR (#3887) I propose changes to the type checker that would allow paths to include applications of pure methods, e.g. x + 1. The examples in that PR’s tests illustrate the syntax a bit more, for instance:

val x = 1
val y: {x} = x
implicitly[{x + 1} =:= {y + 1}]

The implementation of the proposed syntax is included in the PR and turns out to be rather straightforward.

5 Likes
2

What do you think @milessabin ?

3

The change would make a lot of sense if we introduce refinement types (in the sense of F* or Liquid Haskell). A nice syntax for refinement types would be along the following lines:

{ x: Int | x >= 0 }

If we ever take that step it would make perfect sense to have {23} denote a singleton type.

7 Likes
4

At one point the literal types proposal included the ability to use a stable path without the .type suffix to denote the corresponding singleton type. @adriaanm objected for reasons that I can’t recall right now, and unfortunately I can’t track down the discussion.

I’d certainly be in favour of looking at it again.

5

I think that when all stable paths are types, their names will occupy the types namespace as well as the terms namespace. You won’t be able to distinguish between a class and its companion object. And the following idiom won’t work anymore, because type module.Foo can mean the val as well as the type alias:

object module {
  type Foo = internals.FooT[Id]
  val Foo = internals.FooFactory
}
6

I like the idea, but the syntax feels a bit weird to me. Specifically, I’m not a massive fan of that, even in a type context, {} (an empty structural type, effectively a silly way to write AnyRef), {x} (exactly the object x), and {def x: Type} (a structural type containing the method x) all look relatively similar, but would have confusingly different behaviour. And that’s before we even get into that { /* stuff */ } can already be a scope, a lambda, a structural type, and so on.

Perhaps [x] would feel more natural, given that in Scala brackets are already dedicated to mean “special case of type”, and that there is currently no other meaning for brackets without a prefix.

6 Likes