Hi contributors,
@liufengyun and I have been working on a SIP to deal with exhaustivity warnings and “complementary” custom extractors, by introducing sealed types.
Here’s the link to the rendered proposal, but here’s a snippet:
sealed type Num = Int {
case 0 => val Zero
case n if n > 0 => type Pos
case _ => type Neg
}
What do you think?
Hello.
So what the type Num represents ? A Int & [Zero | Pos | Neg] ?
Or Zero, Pos and Neg are subtypes of Int so Num represents an Int ?
match types. Is there a way to unify them?Have a look at the document. In terms of types it desugars into:
type Num = Int
val Zero: Num = 0
opaque type Pos <: Num = Num
opaque type Neg <: Num = Num
No, because match types are Type => Type and we want Value => Type here.
The spectrum is (I used to have this at the start of “Design” but I took it out as too chatty):
| From | To | ||
|---|---|---|---|
| functions: | Value | => | Value |
| match types: | Type | => | Type |
| erasedValue + inline match: | Type | => | Value |
| sealed types | Value | => | Type |
Subtypes must absolutely be defined in the same file. In fact they need to be defined inside the match block, much like you define subtypes inside the block of an enum.
Can this also solve the motivating example from Implement @covers annotation for partial irrefutable specification by liufengyun · Pull Request #11186 · lampepfl/dotty · GitHub? I.e. custom extractors for Seq.
I agree with soronpo. Sealed types and match types are actually unifiable.
I think we should treat the code after the declaration as a normal statement:
type Foo = {
//This Tree must return a type
}
With this change, match types could be written like this:
type LeafElem[X] = X match { //Simple tree with pattern matching
case String => Char
case Array[T] => LeafElem[T]
case Iterable[T] => LeafElem[T]
case AnyVal => X
}
As you can see, the match type definition should not change if we treat type definition as a “normal” Tree.
For value-check, I think we could use a method-like syntax type Foo(original: Int) = {}:
type Num(n: Int) = n match {
case 0 => Zero
case n if n > 0 => Pos
case _ => Neg
}
Note: here we don’t use singleton types because the above example should support non-litteral values.
We should only be able to pass one argument:
val t: Num = 5 //Here 5 is passed as the `n` argument in the above example.
But what’s the aliased/returned type ? I see two options:
For example to make the compiler understand I can use int-related methods on my Num, I could define it like that:
type Num(n: Int) <: Int = n match {
case 0 => Zero
case n if n > 0 => Pos
case _ => Neg
}
Note: here I use <: because it is already used for opaque types and because our type return a subtype of Int.
With this approach, opaque types are some kind of “inline types”. The definition Tree should be inlined:
opaque type Num(n: Int) <: Int = n match { //Inlined match
case 0 => Zero
case n if n > 0 => Pos
case _ => Neg
}
Note: Here n must be inlined. Maybe we should specify inline n: Num ?
This approach allow us to use inline methods like quotes’ error/warning:
opaque type Positive(n: Int) = n match {
case n if n > 0 => Int
case _ => quotes.reflect.report.error(s"$n must be positive.")
}
Finally, using an inlined Tree allow us to use singleton types as value arguments:
import scala.compiletime.requireConst
opaque type Between(n: Int)[A <: Int, B <: Int](n: Int) <: Int = {
val a = requireConst[A]
val b = requireConst[B]
if(n > a && n < b) Int else quotes.reflect.report.error(s"$n must be between $a and $b")
}
val x: Between[0, 5] = 4
val y: Between[0, 5] = 6 //Compile time error
Absolutely, that was the starting point.
I mean the whole file is tree, but I’m not sure how much that can be called things being “unified”. The way I see it is they’re definitely similar, but one fundamental difference in match types and sealed types is that the computation in the match is done at compile time in match types, but at runtime in sealed types (to an ordinal). There needs to be a way to define singleton types, for things like empty/nil/zero, or specific values, such as:
sealed opaque type Permission = Int {
case 1 => val Read
case 2 => val Write
}
which desugars to
opaque type Permission = Int
val Read: Permission = 1
val Write: Permission = 2
extension (p: Permission):
def ordinal: Int = (p: Int) match { case 1 => 0 case 2 => 1 case _ => -1 }
given TypeTest[Int, Read.type] = (n: Int) => if ((n: Permission).ordinal == 0) Some(n) else None
given TypeTest[Int, Write.type] = (n: Int) => if ((n: Permission).ordinal == 1) Some(n) else None
given TypeTest[Int, Permission] = (n: Int) => if ((n: Permission).ordinal == -1) None else Some(n)
given [T <: Permission](using t: TypeTest[Int, T]): TypeTest[Permission, T] = (p: Permission) => t.unapply(p)
and makes the following correctly exhaustive:
(p: Permission) match
case Read =>
case Write =>
Is there a way to implement this as a library in current Scala, e.g. using match types? The syntax construct accompanying the sealed definition feels very heavy and also unique in the language – it’s not a template or anything like any other construct! Having super unique syntax for a very specific construct feels somewhat un-Scalalike to me – even though similar constructs started appearing in Scala 3, they did so after becoming established patterns.
but I’m not sure how much that can be called things being “unified”
I think you’re the “value-type” match types, “type-type” match types and opaque types can be unified and be more flexible as described in my previous post.
and makes the following correctly exhaustive:
(p: Permission) match
case Read =>
case Write =>
I didn’t think about the exhaustivity of external matches. This problem can be fixed by just adding the sealed keyword:
sealed type Num(n: Int) <: Int = n match {
case 0 => Zero
case n if n > 0 => Pos
case _ => Neg
}
Here, sealed should just have the same exact effect as used on trait.
PS: The last sentence’s english might not be correct. I’m not english native and i’m not sure about the wording.
Very interesting idea.
Not sure if it’s a bug in the SIP example but you have:
given TypeTest[Int, Num] = (n: Int) => if ((n: Num).ordinal == -1) None else Some(n)
where as you’re proposing to synthesise:
extension (n: Num):
def ordinal: Int = (n: Int) match {
case 0 => 0
case n if n > 0 => 1
case _ => 2
}
which will never return -1. Is this because the sugared declaration has a catch-all in it, and that a catch-all of -1 would be synthesised otherwise, or something?
Good catch - no, that’s a mistake: as every Int is a Num that test can never fail, so the if can go. I’ll amend it, thank you.
[edit] Just to expand: that -1 and using it in the TypeTest is there for subset partitioning, such as peano numbers.
I’m confused by what you mean. The intent is that Read and Write as singleton values, and thus their types Read.type and Write.type, are the complete set of subtypes of Permission. So the exhaustivity checker can use that fact and not warn in that example.
I believe not, which is why I’m proposing this. As I put in Design, you can’t define a sealed hierarchy for anything that isn’t a class, so you can’t define your own sealed subtype hierarchy for an existing type like Int or String. Also match types only operate on types, so how are you going to define a branch in a match type for the case case xs if xs.isEmpty (using the LazyList example)?
It’s the part I’ve put the most time in. I went with something that is relatively terse, but trying to reuse well known and understood syntax pieces, borrowing mostly from enum, match, and match type syntax. One constraint I established is that the match logic and the types must live as one, in order for the exhaustivity of the subtypes to be clear by construction.
I’m not sure what you mean by “established patterns” but having built up a number of cases of unfortunate exhaustivity in custom extractors (LazyList, :+, +:, etc), as well as the inability to define exhaustivity for opaque types (Permission) or abstract types (Peano’s Nat) I went looking for tools and found there was nothing even in Scala 3 for the Value => Type variant I needed. So it is unique, but it’s very similar too.
My english might be broken but that’s what I meant.
If we treat type definitition as normal statement, we will not need special syntax but the sealed keyword.
Lets pick this example:
type Num(n: Int) <: Int = n match {
case x if x > 0 => Pos
case 0 => Zero
case _ => Neg
}
To make match on the type Num exhaustive, I have to just mark my type as sealed:
sealed type Num(n: Int) <: Int = n match {
case x if x > 0 => Pos
case 0 => Zero
case _ => Neg
}
We can unify match types and sealed types. No need to make 2 different syntaxes.
Another key difference between a match type and a sealed type is that a match type is a type-level mapping from existing types to existing types, while a sealed type (like an enum) is defining types (actually subtypes). That’s why match types don’t need to deal with how to distinguish non-singleton types and singleton types, which I’m doing with val Zero and type Pos. So match type syntax isn’t enough.
It’s an interesting idea to bridge sealed types with the hypothetical “term-match” types.
If we tweak it a little bit, the following code might be closer to what you propose:
type Num(n: Int) <: Int = n match {
case x if x > 0 => Pos
case 0 => Zero
case _ => Neg
}
// with explicit type definitions
type Pos <: Num
type Zero <: Num
type Neg <: Num
Despite the syntactic similarity, there are major differences:
sealed types.sealed types use the syntax but desugars to code that has runtime semantics.Num(n), while for sealed types we can use Num alone.The syntactic similarity does not hold semantically. That said, I do agree there’s room to improve the syntax of the proposal. But semantically, if we want a high-level design for the feature, the current proposal seems to be a logical consequent.
Thanks for the proposal, it looks really great!
The one thing that seems a bit irregular is the val.
given
sealed type Num = Int {
case 0 => val Zero
case n if n > 0 => type Pos
case _ => type Neg
}
the Zero is never seen again. I would expect
(n: Int) match
case Zero =>
case x: Pos =>
case x: Neg =>
which matches on the thing on the right side of the =>, rather than
(n: Int) match
case 0 =>
case x: Pos =>
case x: Neg =>
Will both work? Should both work?
Alternatively, if it should remain case 0, do we have to name the case in the sealed type, or should there maybe be a way to let that remain anonymous, since we’re not using the name again anyway?
Good questions. Yes, both should work, in my mind. I’m not sure about the anonymous option, but perhaps it’s fine?
sealed type Num = Int {
case 0 =>
case n if n > 0 => type Pos
case _ => type Neg
}