It is in fact invariant in τ, because τ appears in both codomain and domain
positions. Concretely, although nat is a subtype of int, for example,
neither of (unit -> nat) * (nat -> unit) and (unit -> int) * (int -> unit)
is a subtype of the other. Let N denote the first of these types and I the
second; then a function expecting N like λ (p : N) nat_sqrt((p·l)(())) can
have undefined behavior when applied to a term of type I like
(λ (_ : unit) -4, λ (_ : int) ()), so I is not a subtype of N.
Symmetrically, we cannot safely apply λ (p : I) (p·r)(-4) to the value of
type N (λ (_ : unit) 3, λ (n : nat) (λ (_ : nat) unit)(nat_sqrt(n)))
(assuming an eager dynamics), so N is not a subtype of I.
Let r_1 be the ρ_1 value fold((eq -> λ (_ : ρ_1) true) and r_2 be the
ρ_2 value fold((eq -> λ (o : ρ_2) unfold(o)·f, f -> true)). Then it is
unsafe to pass r_2 to the function λ (o : ρ_1) (unfold(o)·eq)(r_1), because
doing do will reduce to the expression unfold(r_1)·f, which will get stuck
immediately after unfolding r_1.
We associate to every subtyping derivation a term χ, such that a derivation
of τ <: τ' produces a term χ : τ -> τ'.
χ be λ (x : τ) x.χ_1 : τ'' -> τ' and
χ_2 : τ' -> τ are the coercions associated to the subderivations, let χ
be λ (x : τ'') χ_2(χ_1(x)).χ be
λ (p : <i_1 -> τ_i, ..., i_n -> τ_n>) (j_1 -> p·j_1, ..., j_m -> p·j_m)).χ_i is the coercion
associated to the derivation of the premise τ_i' <: τ_i, let χ be
λ (p : <i_1 -> τ_i_1', ..., i_n -> τ_i_n'>)
(i_1 -> χ_i_1(p·i_1), ..., i_n -> χ_i_n(p·i_n))χ_i is the coercion
associated to the derivation of the premise τ_i' <: τ_i, let χ be
λ (s : [i_1 -> τ_i_1', ..., i_n -> τ_i_n'])
case s {i_1·x -> i_1·χ_i_1(x) | ... | i_n·x -> i_n·χ_i_n(x)}χ_1 is the
coercion associated to the derivation of the premise τ_1' <: τ_1 and χ_2
the coercion associated to the derivation of the premise τ_2' <: τ_2, let
χ be λ (f : τ_1 -> τ_2') λ (t_1' : τ_1') χ_2(f(χ_1(t_1'))).It’s not entirely clear to me what (b) is supposed to mean. To “apply
subsumption” to e : τ is an action that derives a new typing judgment from
the old one, which cannot modify the term. I can imagine a method of
interpretation where typing judgments are compiled to terms in a subtyping-free
language, and instances of the subsumption rule get compiled to applications of
coercions…
I think that the above system is probably coherent. A handwavy proof sketch would go along the lines of:
τ <: τ', then τ and τ' have the same type constructor (sum,
function, etc).τ <: τ'
can be inverted into a sequence of rules for τ’s constructor, connected by
cases of (24.1).These proofs go through without needing induction, thanks to the flattened structure of the transition relation enabled by the use of a stack.
s is k |> ifz{e_0; x.e_1}(e) and s' is
k; ifz{e_0; x.e_1}(-) |> e. Inverting s ok gives us k <|: τ and
ifz{e_0; x.e_1}(e) : τ for some τ, and inverting the latter tells us
that e : nat, e_0 : τ, and x : nat |- e_1 : τ. We can then derive
s' ok using rules (28.9a), (28.7b), and (28.8b).s is k; ifz{e_0; x.e_1}(-) <| z and s' is k |> e_0.
Inverting s ok gives us k; ifz{e_0; x.e_1}(-) <|: nat, and inverting
that gives us k <|: τ and e_0 : τ. We can then derive s' ok using
rule (28.9a).s is k; ifz{e_0; x.e_1}(-) <| s(e) and s' is
k |> [e/x]e_1. Inverting s ok gives us
k; ifz{e_0; x.e_1}(-) <|: nat, and inverting that gives us k <|: τ
and x : nat |- e_1 : τ. We can then derive s' ok using rule (28.9a)
and the standard properties of typings of substitutions.s. If it is an evaluation
state k |> e, then it can always take a step—check the form of e, and
there will be exactly one applicable rule for that form. If it is a return
state k <| e, then consider the form of k. Progress is proved for each
form by inverting the s ok judgment. In the case where s is
k; ifz{e_0; x.e_1}(-) <| e, inverting this judgment and its premises gives
e : nat, and e val. By these first two consequences, e must be either
z or s(e'), in which case either (28.4b) or (28.4c) can be applied to
get s |-> s'.For a call-by-value variant, we’d need to replace rule (28.5c) so that the
argument is evaluated next instead of immediately substituted. In order to do
this, we need a new type of stack frame of the form ap(lam{τ}(x.e); -) to
store the evaluated function while its argument is being evaluated. Then we can
replace (28.5c) with the following two rules:
k; ap(-; e_2) <| lam{τ}(x.e) |-> k; ap(lam{τ}(x.e); -) |> e_2
k; ap(lam{τ}(x.e); -) <| v |-> k |> [v/x]e
We also add a new rule to the statics to account for this type of frame:
x : τ |- e : τ'
----------------------------
ap(lam{τ}(x.e); -) : τ ~> τ'