Access the predicate of a SubSet type directly

[seebees]

I find SubSet types to be very useful.
However it can be very useful to have access to the predicate that defines the Subset Type.
Like this:

predicate IsFoo(){}
type Foo = b: Bar
| IsFoo(b)
witness *

For the most part this works nicely,
but for either very simple Subset Types or very important ones
it would be nice to have a single source of truth.

Dafny already has some simple sugar for datatype

datatype Baz =
| Qux
| Corge
| Grault

var baz: Baz

if baz.Corge? then
// Do something

I would like to see something similar for Subset types

type Foo = b: Bar
|
  && Important(b)
  && Things(b)
  && AboutBar(b)
witness *

// This bar should also be a Foo given how I got it
var bar: Bar

// So I would like to be able to do something like:
assert Foo?(bar);

The obvious question: Can the be used at runtime?
I say no, unless someone wants to contemplate type method Foo....
Which is so ridiculous that it makes me chuckle :)
I don't think that Subset Types are ever... "compiled"
so I would not complicate things by adding some halfsies condition.

[MikaelMayer]

We can definitely detect if the constraint of a subset type is compilable or not, actually, we are working on that in #1604
Based on #1555, I'd say the correct wording to ensure a constraint is compilable would be compiled type
And your idea is a good one in principle. Moreover the function Foo? could actually be a ghost function if the constraint was not compilable.
How much would it enhance readability in your projects?

[cpitclaudel]

FWIW, Foo? sounds like a great idea to me; I was surprised to find that there was no way to access the predicate. I would expect it to be ghost by default.

I hoped that x is Foo would work, but it would be surprising for that to be ghost, I think.

[seebees]

The reason it would be nice for Dafny to offer this sugar
is not that this is significantly more readable,
since I could currently create such predicates,
but that makes these two concepts <==>.

That is, I can evolve a named predicate,
but someone could also add some additional condition to the Subset type.
It is very unlikely that such a change would work everywhere,
but this would make the error and the change clearly tied.

Given:

predicate Foo?(b: Bar) {
  && Important(b)
  && Things(b)
  && AboutBar(b)
}
type Foo = b: Bar
| Foo?(b) && Woops(b)
witness *

The error should clearly be at the assert not the OnlyTakeFoo call site.

// Lots of code
var b := GetMeABar();
// More logic
assert Foo?(b);
// Doing things
OnlyTakeFoo(b);

[MikaelMayer]

I get your point now, for maintainability. It makes better sense.

I like both syntaxes X is Foo and Foo?(X). I start to think we should have Foo?(X) first, because it does not feels like X is Foo has requires, whereas it's acceptable that Foo?(X) can have preconditions (that X is a Bar)

Either way, we could start with one and define the other with it. For example, if Foo?(X) is the ground truth, we can define X is Foo would be resolved as var x := X; x is Bar && Foo?(x)
On the other way round, x is Foo would resolve to the expression that var x := X; x is Bar && InlinedFooConstraint(x)
One problem with inlining the constraint all the time is that it cannot be "cached" nor "traced".