Next-gen subset type

[MikaelMayer]

We know we can do the following refactoring

class A {
  predicate Valid()
}
method do(a: A) returns (aa: A)
  requires a.Valid()
  ensures aa.Valid()

to:

class A_ {
  predicate Valid()
}
type A = a: A_ | a.Valid()
method do(a: A) returns (aa: A)

and we all like it. It is striking that putting the validation code inside the type name makes the methods more legible, and less specification error-prone.
I am thinking of a generalization of subset types, a kind of dependent types, which would enable the following refactoring:

class C ...
method do(a: A, b: B) returns (c: C)
  ensures abcPredicate(a, b, c)

==>

class C_ ...
type C(a: A, b: B) = c: C_ | abcPredicate(a, b, c)
method do(a: A, b: B) returns (c: C(a, b))

With such type declaration, it would enable to ensure we never return a C without it being built from some a and some b, and hold an invariant.
An idea to discuss.

[mschlaipfer]

Would something like

class A
  invariant this.Valid()
{
  predicate Valid()
}
method do(a: A) returns (aa: A)

work?

[MikaelMayer]

That's another interesting language feature request and I love it! When reading it I initially thought "oh I did not know this nice syntax in Dafny but it makes sense" until I realized it's actually not there yet at all.
How much would this be useful to you?

[mschlaipfer]

Not sure we do this for class, but for datatype we have this pattern you use above and there we need to invent a name for a type we then never use (we only need the subset type with the invariant). I think invariants attached directly to types would be nice to have.

[kjx]

I blame Matthew Parkinson.

well only partly. (for those who don't know me in person, that's a joke -
and an acknowledgement that his ideas here were pretty influential).

https://people.dsv.su.se/~tobias/iwaco/p3-parkinson.pdf

the question is do you conjoin the invariant with method specs,
or have a name for it that can conjoin it, or have some other way
to say "this method doesn't need the class invariant"

I didn't know the constraints on algebraic types worked.
will play with them again.

[MikaelMayer]

Dafny 4.0

• type are just syntactic sugar for predicate
• newtype are just syntactic sugar for opaque predicate

Here is why and how it could be transformative.
Currently, we define a subset type like this

type MyInt = x : int | 0 <= x < 13 witness *

Consider a 'desugared' version of MyInt:

predicate type MyInt(x: int) {
  0 <= x < 13
} witness *

Wow, it looks like we only need to add witness ... to the predicate to make it actually supersede type !
Conversely, given any predicate without requires could be used as a subset type.

Interesting note: Predicates having more than one argument would be refinement types.

For example:

predicate type LessThan(j: int, i: int) {
  j < i
} witness (0, 1)

would enable us to modify:

method returnLower(i: int) returns (j: int)
  ensures LessThan(i, j) { .... }

to the following, arguably "simpler":

method returnLower(i: int) returns (j: LessThan(i)) { ... }

Now, here is how we could use it

method test() {
  var i := ...
  var j: LessThan(i) = returnLower(i);
  // The type is the predicate. If the predicate is a predicate method,
  // we can test it, else it's only in specification
}

[MikaelMayer]

Another interesting consequence of predicate type, especially when they are compiled predicate type
If there is a predicate type SubA(x: A) { ... }, then the following expression

x is T

could either be rewritten, both in ghost or compiled contexts:

SubA(x) or x is A && SubA(x)

[MikaelMayer]

Another much simpler and intermediate way to implement predicate types would be that

predicate type Pred(a: T) {
  Body
} witness X

actually simply desugars, for the resolver, verifier and compiler, to

predicate Pred(a: T) {
  Body
}
type Pred = a : T | Pred(a) witness T

That way, it would still provide one source of truth that would resolve #1680.