LF Subordination¶
LF declarations in Beluga may or may not refer to earlier declarations. Therefore, it is possible to ascertain that certain derivations cannot depend on certain contextual assumptions, and to eliminate these assumptions. As a concrete example, consider this signature.
LF unit1 : type =
| u1 : unit1
;
LF unit2 : type =
| u2 : unit2
;
schema ctx = block a1 : unit1, a2 : unit2 ;
The schema ctx
consists of blocks (pairs) consisting of a unit1
and a
unit2
. Now suppose we have a derivation of type
g, b : block a1 : unit1, a2 : unit2 |- unit1
where g : ctx
.
This derivation builds a unit1
, and by looking at the definition of that
type, we can see that there is no way any unit2
could be involved in the
construction of that derivation.
Strengthening¶
Beluga recognizes as legitimate any program that would drop such irrelevant
assumptions: this is called strengthening.
In Harpoon this is accomplished by using the strengthen
tactic. In a Beluga program, one uses pattern matching together with
an explicit substitution that witnesses the strengthening. Suppose in the below
example that x : [g, b : block a1 : unit1, a2 : unit2 |- unit1]
. To
strengthen this, one would use a construction as follows.
let [g, b : block a1 : unit1, a2 : unit2 |- X[.., b.1]] = x in ...
The synthesized type for X
would be g, x1 : unit1 |- unit1
. This is
somewhat confusing because the substitution that witnesses the strengthening
here is in fact a substitution that weakens X
.
Beluga’s subordination analysis over the loaded signature accounts for
transitive dependencies between LF declarations. Beluga will consider
strengthening notably during coverage checking as well as when synthesizing the
type of unknowns, written as _
in LF terms.