Feat: Predicate types #8
Conversation
Create 0004-predicate-types.md
| - For every subset type `MyType`, we could also generate by default a predicate with the name `MyType?` that has the same constraint. | ||
| That might actually be even simpler, but then there would be no control over the predicate like `{:opaque}` and `reveal`. |
There was a problem hiding this comment.
Of various alternatives, I think this is the strongest contender.
| [drawbacks]: #drawbacks | ||
|
|
||
| * It feels odd to have restrictions on a predicate so that it becomes a type. | ||
| * It might be even more confusing for newcomers. |
There was a problem hiding this comment.
To teach beginners, I'm guessing it will be preferable to first teach about subset types and about predicates. When those two concepts are clearly understood, one can introduce predicate type, which then acts just like a shorthand.
| # Prior art | ||
| [prior-art]: #prior-art | ||
|
|
||
| This feature to combine both the predicate and a subset type in a single construct does not exist in other programming languages, as far as I know. |
There was a problem hiding this comment.
A related issue are Dafny's least predicates, which are predicates in Dafny and are data in Coq (declared as Inductive).
The theorem prover PVS has predicate subtypes. I'm unsure, but it may also have a syntax that lets you combine the predicate and the type (either like the predicate type here or as an Odd? predicate that is automatically generated from a type Odd, like in the example below).
| # Motivation | ||
| [motivation]: #motivation | ||
|
|
||
| The last snippet above is very common: We define a predicate, and use that predicate to define a subset type. |
There was a problem hiding this comment.
Another common idiom is
datatype D_ = ... {
predicate Valid() { ... }
}
type D = d: D_ | d.Valid()Does predicate type offer any advantage here?
There was a problem hiding this comment.
Very good question. It would, but only if we were able to define types in datatype definitions, e.g.
datatype D = ... {
predicate type Valid() { ... }
}
function f(d: D.Valid) { ... }
that would desugar to
datatype D = ... {
predicate Valid() { ... }
static type Valid = d: D | d.Valid();
}
function f(d: D.Valid) { ... }
No description provided.