I will write down here my ideas about how to deal with refinements properly.
First, the current state of affairs is that an (atomic) refinement (like - true / - inh) is specified in your LF signature with sort SORT. This is not satisfactory, because the states of the refinement engine will not be well-typed: instead, we want to have some notion of refinement that lies over the existing signature, and then presuppose that input states to the refinement engine typecheck at the LF sort that the refinement refines, etc.
I think that the simplest thing to do for now is to define a refinement signature as a mapping of symbols/names to LF arities; for instance, we would map inh to (arity ([A exp]) exp).
[Refinements are not dependent: that is, you can't use a refinement when assigning an arity to a refinement. Doing so would correspond to adding support for presuppositions to our framework, and might be interesting in the future, but I think we should not try to account for this at this time, since it's not yet quite clear how to make it work (though I can think of a few interesting ideas).]
Things like inh generate the atomic refinements, like (plug inh bool), which refine LF sorts (in thie case exp); then, on top of this, we generate the general refinements, which refine LF arities, in a compositional way.
All this give rise to a grammar of "valid" refinements with respect to an LF signature Γ and a refinement signature that lies over Γ. In addition, it gives rise to an erasure of refinements into LF arities.
Finally, when we define a PRL, we would do something like ambiently set the current LF signature and refinement signature, and using this, we could add contracts (or some other kind of check) to ensure that the user's defined rules preserve well-typedness.
I will write down here my ideas about how to deal with refinements properly.
First, the current state of affairs is that an (atomic) refinement (like
- true/- inh) is specified in your LF signature with sortSORT. This is not satisfactory, because the states of the refinement engine will not be well-typed: instead, we want to have some notion of refinement that lies over the existing signature, and then presuppose that input states to the refinement engine typecheck at the LF sort that the refinement refines, etc.I think that the simplest thing to do for now is to define a refinement signature as a mapping of symbols/names to LF arities; for instance, we would map
inhto(arity ([A exp]) exp).[Refinements are not dependent: that is, you can't use a refinement when assigning an arity to a refinement. Doing so would correspond to adding support for presuppositions to our framework, and might be interesting in the future, but I think we should not try to account for this at this time, since it's not yet quite clear how to make it work (though I can think of a few interesting ideas).]
Things like
inhgenerate the atomic refinements, like(plug inh bool), which refine LF sorts (in thie caseexp); then, on top of this, we generate the general refinements, which refine LF arities, in a compositional way.All this give rise to a grammar of "valid" refinements with respect to an LF signature
Γand a refinement signature that lies overΓ. In addition, it gives rise to an erasure of refinements into LF arities.Finally, when we define a PRL, we would do something like ambiently set the current LF signature and refinement signature, and using this, we could add contracts (or some other kind of check) to ensure that the user's defined rules preserve well-typedness.