Cheap functors

Right now, if both Y.fsti and Y.fst exist, then fstar Y.fst will check the interleaving of Y.fst and Y.fsti (see F★ interfaces (split file, more complicated version)).

Assume the existence of Y.fst, I.fsti, F.fst, and M.fst. The proposal is as follows.

Checking that module Y satisfies interface I

Y.fst:

module Y: I
// contents of module Y

Semantics: fstar Y.fst will check the interleaving of Y.fst and I.fsti.

Any reference to Y from another module will figure out that Y has been ascribed to I; such a reference "sees" I, not the implementation of Y. (JP: dubious)

Parameterizing F over a module X satisfying I

F.fst:

module F(X: I)

X is a name, I is a reference to I.fsti.

Semantics: this is desugared to

module F
module X = I

Instantiating F with Y

M.fst:

module M = F(Y)

Semantics: this desugars to

module M
[Y/X]F // substitute Y for X in F

or more prosaically:

module M
module X = Y
// contents of F

Use-case of several interfaces K ⊆ J ⊆ I

module Y: K

(check that it implements the most precise interface)

Then, this just performs an interleaving, provided that (and this is unchecked) I, J and K are a succession of refinements:

module F(X: I)

module M = F(Y)

The functor and ST

If we want to use multiple heap models, then each one of them has to define its own reference type. In particular, for hyperheaps, we would need to upgrade to a dependent pair of a reference and the region it lives in. This would be some non-trivial amount of work.