Terminology question

[martinberger]

Sail offers types of the form {'tv1 'tv2 ... 'tvn, constraints. t}. In the refinement type literature those have been given many names (e.g. constrained type, predicate subtype, subtype, subset, refined sorts and refinement predicate). I have been calling them existential types, but that may be misleading as there is no clear duality with Sail's forall. What's the preferred term in the Sail community? Patrick Rondon, in his PhD work which introduced liquid types, calls them "refinement types", but liquid types don't encompass all of refinement types. I think we should standardise, especially as there is now a lot of work in this direction, including Liquid Haskell, and Liquid Rust.

I'm asking because having an agreed upon term is a first step towards better explaining how they work in Sail. We could even have a corresponding entry in https://alasdair.github.io/ (that I would be happy to write).

[Alasdair]

I normally refer to them as existential types. They are basically the same thing as refinement types, but I think the syntax is a bit different than a typical presentation of refinement types, as they are stated as "there exists these type variables such that..." rather than as a refinement.

Note that {'tv1 'tv2 ... 'tvn, constraints. t} could have been exists 'tv1 'tv2 ... 'tvn, constraints. t, but existentials can appear in more places in the grammar than forall, so the lack of a closing delimiter was an issue. They also behave like existentials, so

val ex1 : forall 'n, 'n > 0. int('n) -> unit

val ex2 : {'n, 'n > 0. int('n)} -> unit

are the same, which corresponds to ∀x. (P(x) -> Q) <-> (∃x. P(x)) -> Q in logic.

[martinberger]

val ex2 : {'n, 'n > 0. int('n)} -> unit

This should be val ex2 : {'n, 'n > 0. int('n)} I guess.

[martinberger]

OK decision made, I will keep calling them existential types.

Sail programs would be infinitely more grep-able if there was a keyword exists rather than {...}. The problem of closing could be solved by having e.g. exists 'n, constraints.{...}, and symmetrically forall 'n, constraints.{...}

[Alasdair]

val ex2 : {'n, 'n > 0. int('n)} -> unit

This should be val ex2 : {'n, 'n > 0. int('n)} I guess.

The -> unit was intended. Internally an existential on the left-hand side of a function arrow will be canonicalised to the forall equivalent, but it does work like it should.

[martinberger]

Internally an existential on the left-hand side of a function arrow will be canonicalised to the forall equivalent, but it does work like it should.

I'm not 100% sure I fully understand what that means. The function space constructor is contravariant in the first argument, so how does the semantics work?

[martinberger]

Now that we are talking about the relationship of forall and exists in Sail, what are the constraints on nesting them? With higher-ranked types, you are quickly approaching the danger zone of undecidability.

Are there clear syntactic restrictions?

[Alasdair]

There currently aren't any clear syntactic restrictions, other than that forall can only appear in function types. Existentials are allowed anywhere a type can appear. If nesting existentials would ever lead us to generate constraints during type checking that involve nested quantifiers that's when they are rejected.

If we had function subtyping, then {'n. int('n)} -> unit would be a subtype of {'n, 'n > 0. int('n)} -> unit, when {'n, '> 0. int('n)} is a subtype of {'n. int('n)} which is contravariance, but forall 'n. (int('n) -> unit) would also be subtype of forall 'n, 'n > 0. (int('n) -> unit) (brackets added for clarity), for the same reason, so it seems like the property of lifting an existential out of the left-hand side of a function arrow to a universal quantifier over the entire function arrow is orthogonal to contravariance?

[Timmmm]

Internally an existential on the left-hand side of a function arrow will be canonicalised to the forall equivalent, but it does work like it should.

Interesting! Does that mean forall is technically redundant?

[Alasdair]

If you need to quantify over both an input type and an output type you still need it, forall 'n. int('n) -> int('n)