Var x, y, z
Term s, t ::= x variable
λx:T.t term abstraction
s t term application
new(x: T)d record creation
t.l term member selection
Definition d ::= { a = t } term member
{ A = T } type member
Value* v, w ::= λx:T.t
new(x: T)d
Path* p, q ::= x
v
Type S, T, U ::= ⊤ top
⊥ bottom
S ∧ T intersection
(x:S) → T dependent function type
{ a : T } term member
{ A :: K } type member
μ(x: T) recursive record type
p.A type member selection
λx:S.T type abstraction
S t type application
Kind K ::= (x:S) → K dependent function kind
S..T type interval kind
Context Γ ::= ∅ empty
Γ, x: T extension
* = predicate on terms defining a subset of the terms
As is customary, we write S → T
as a shorthand for non-dependent
function types (and kinds), i.e. for (x: S) → T
where x
does not
appear freely in T
. We write *
for the interval containing the
entire type lattice, i.e. for ⊥..⊤
.
Substitutions [x := p]
of a variable x
for a path p
and their
applications t[x := p]
to terms and T[x := p]
to types are defined
in the usual way.
We make use of let
-binders, which are desugared in the usual way,
⟦ let x: T = t₁ in t₂ ⟧ = (λx: T. ⟦ t₂ ⟧) ⟦ t₁ ⟧
omitting the explicit type annotation when it can be readily inferred.
As in DOT, parametric polymorphism is achieved through "boxing" and (path-)dependent types, e.g. universals are encoded as
∀X.T = (x: { A :: * }) → T[X := x.A]
ΛX.t = λx: { A :: * }. t[X := x.A]
Type operators are encoded similarly as
K₁ → K₂ = { A :: K₁ } → K₂
λX: K. T = λx: { A :: K }. T[X := x.A]
Note that we can use dependent kinds to give very precise kinds to type operators:
λX: K. T :: (X: K) → T..T
As we'll see below, this allows us to admit β-reductions in types through a combination of kinding and sub-kinding.
Contractions:
(AppAbs) (λx:T.t) v —→ t[x := v]
d = … ∧ { a = t } ∧ …
(RecSel) ------------------------------------
(new(x: T)d).a —→ t[x := new(x: T)d]
Congruence:
t₁ —→ t₂'
(App₁) ---------------
t₁ t₂ —→ t₁' t₂
t —→ t'
(App₂) -----------
v t —→ v t'
t —→ t'
(Sel) -----------
t.a —→ t'.a
x : T ∈ Γ
--------- (T-Var)
Γ ⊢ x : T
Γ ⊢ S :: * Γ, x : S ⊢ t : T
------------------------------ (T-→-I)
Γ ⊢ λx: S.t : (x: S) → T
Γ ⊢ t : (x: S) → T Γ ⊢ p : S
------------------------------ (T-→-E₁)
Γ ⊢ t p : T[x := p]
Γ ⊢ t₁ : S → T Γ ⊢ t₂ : S
--------------------------- (T-→-E₂)
Γ ⊢ t₁ t₂ : T
Γ, x: T ⊢ d : T
------------------------ (T-{}-I)
Γ ⊢ new(x: T)d : μ(x: T)
Γ ⊢ t : { a : T }
----------------- (T-{}-E)
Γ ⊢ t.a : T
Γ ⊢ p : T[x := p]
--------------------- (T-Fold)
Γ ⊢ p : μ(x: T)
Γ ⊢ p : μ(x: T)
--------------------- (T-Unfold)
Γ ⊢ p : T[x := p]
Γ ⊢ t: T Γ ⊢ t: U
--------------------
Γ ⊢ t: T ∧ U
Γ ⊢ t : S Γ ⊢ S <: T
---------------------- (T-Sub)
Γ ⊢ t : T
Value/path typing is defined as the obvious restrictions of the above relation to values/paths.
The following rules for let
-binders are admissible.
Γ ⊢ p : S Γ, x : S ⊢ t : T
--------------------------------- (T-Let₁)
Γ ⊢ let x: S = p in t : T[x := p]
Γ ⊢ t₁ : S Γ ⊢ t₂ : T
--------------------------- (T-Let₂)
Γ ⊢ let x: S = t₁ in t₂ : T
Γ ⊢ t : T
------------------------- (D-{:})
Γ ⊢ { a = t } : { a : T }
Γ ⊢ T :: K
-------------------------- (D-{::})
Γ ⊢ { A = T } : { A :: K }
Γ ⊢ d₁ : T₁ Γ ⊢ d₂ : T₂
--------------------------- (D-∧)
Γ ⊢ d₁ ∧ d₂ : T₁ ∧ T₂
---------- (T-Refl)
Γ ⊢ T <: T
Γ ⊢ S <: T Γ ⊢ T <: U
------------------------ (T-Trans)
Γ ⊢ S <: U
Γ ⊢ T :: *
---------- (T-<:-⊤)
Γ ⊢ T <: ⊤
Γ ⊢ T :: *
---------- (T-⊥-<:)
Γ ⊢ ⊥ <: T
-------------- (T-∧-<:₁)
Γ ⊢ T ∧ U <: T
-------------- (T-∧-<:₂)
Γ ⊢ T ∧ U <: U
Γ ⊢ S <: T Γ ⊢ S <: U
------------------------ (T-<:-∧)
Γ ⊢ S <: T ∧ U
Γ ⊢ S₂ <: S₁ Γ, x: S₂ ⊢ T₁ <: T₂
----------------------------------- (T-→-<:-→)
Γ ⊢ (x: S₁) → T₁ <: (x: S₂) → T₂
Γ ⊢ T₁ <: T₂
---------------------------- (T-{:}-<:-{:})
Γ ⊢ { a : T₁ } <: { a : T₂ }
Γ ⊢ K₁ <:: K₂
------------------------------ (T-{::}-<:-{::})
Γ ⊢ { A :: K₁ } <: { A :: K₂ }
Γ ⊢ S :: T₁..T₂
----------------- (T-..-<:)
Γ ⊢ T₁ <: S
Γ ⊢ S :: T₁..T₂
------------------ (T-<:-..)
Γ ⊢ S <: T₂
---------- (K-⊤-F)
Γ ⊢ ⊤ :: *
---------- (K-⊥-F)
Γ ⊢ ⊥ :: *
Γ ⊢ T, U :: *
-------------- (K-∧-F)
Γ ⊢ T ∧ U :: *
Γ ⊢ S :: * Γ, x: S ⊢ T :: *
------------------------------ (K-→-F)
Γ ⊢ (x: S) → T :: *
Γ ⊢ T :: *
------------------ (K-{:}-F)
Γ ⊢ { a : T } :: *
------------------- (K-{::}-F)
Γ ⊢ { A :: K } :: *
Γ, x: T ⊢ T :: *
---------------- (K-μ-F)
Γ ⊢ μ(x: T) :: *
Γ ⊢ T :: *
------------- (K-..-I)
Γ ⊢ T :: T..T
Γ ⊢ S :: * Γ, x: S ⊢ T :: K
------------------------------ (K-→-I)
Γ ⊢ λx: S.T :: (x: S) → K
Γ ⊢ S :: (x: T) → K Γ ⊢ p : T
------------------------------- (K-→-E₁)
Γ ⊢ S p :: K[x := p]
Γ ⊢ S :: T → K Γ ⊢ t : T
-------------------------- (K-→-E₂)
Γ ⊢ S t :: K
Γ ⊢ p : { A :: K }
------------------ (K-Sel)
Γ ⊢ p.A :: K
Γ ⊢ T :: K₁ Γ ⊢ K₁ <:: K₂
---------------------------- (K-Sub)
Γ ⊢ T :: K₂
Γ ⊢ S₂ <: S₁ Γ ⊢ T₁ <: T₂
---------------------------- (K-..-<::-..)
Γ ⊢ S₁..T₁ <:: S₂..T₂
Γ ⊢ T₂ <: T₁ Γ, x: T₂ ⊢ K₁ <:: K₂
------------------------------------ (K-→-<::-→)
Γ ⊢ (x: T₁) → K₁ <:: (x: T₂) → K₂
A few points worth noting:
-
The selection subtyping rules from DOT are now admissible, e.g. we have
Γ ⊢ p : { A :: S..T } --------------------- (K-Sel) Γ ⊢ p.A :: S..T --------------- (T-..-<:) Γ ⊢ S <: p.A
-
β-reduction in types is also admissible (as a subtyping rule), e.g. we have
Γ ⊢ S :: * Γ, x: S ⊢ T :: T..T --------------------------------- (K-→-I) Γ ⊢ λx: S. T :: (x: S) → T..T Γ ⊢ p : S ----------------------------------------------------- (K-→-E₁) Γ ⊢ (λx: S. T) p :: (T..T)[x := p] ---------------------------------- (T-<:-..) Γ ⊢ (λx: S. T) p <: T[x := p]
Note that this is not a new idea, Aspinall already noted in 1994 that β-reduction is admissible in systems with singleton types1. Type interval kinds can be understood to be a generalization of singleton kinds2: clearly, every singleton
{T}_*
can be encoded as a singleton intervalT..T
. Most of the literature on the properties of systems with singleton types and kinds seems to use PER-semantics1, 2, 3, interpreting singleton types/kinds{T}_K
as an equivalence class of types/kinds up to β(η)-equivalence. -
Types in this system do not have normal forms in general. Consider e.g. the encoding of
{ type F[X] = F[F[X]] }
which is expressible as
new(z: { F :: (x: {A::*}) → z.F (z.F x) .. z.F (z.F x) }) { F = λx:{A::*}. z.F (z.F x) }
This is in contrast to the calculi with singleton kinds proposed by Stone and Harper2, where type equivalence is show to be decidable via comparison of WHNFs.
-
The introduction rule for interval kinds (over proper types)
Γ ⊢ T :: * ------------- (K-..-I) Γ ⊢ T :: T..T
corresponds roughly to Aspinall's
{}-I
for singleton types,1Γ ⊢ M : A ------------- ({}-I) Γ ⊢ M : {M}_A
and Stone and Harper's introduction rule for singleton kinds.2
Γ ⊢ A :: * ------------- Γ ⊢ A :: S(A)
-
One might wonder why we don't give the "most precise" kinds to proper types in the first place, e.g. the kinding rule for the top type could be
------------- (K-⊤-F′) Γ ⊢ ⊤ :: ⊤..⊤
On a first glance, it seems like the original (K-⊤-F) rule could then be recovered via subsumption, since
⊤..⊤ <:: *
. However, a derivation of this relationship already requires one for⊤ :: *
or⊥ :: *
, and so we end up with a circular dependency:??? ---------- Γ ⊢ ⊤ :: * ---------- (T-⊥-<:) ---------- (T-Refl) Γ ⊢ ⊥ <: ⊤ Γ ⊢ ⊤ <: ⊤ -------------------------------- (K-<:-..) Γ ⊢ ⊤..⊤ <:: ⊥..⊤
-
It's questionable whether identifying
*
with⊥..⊤
is a good idea. Alternatively, one could treat them separately and add sub-kinding rules to convert between them. At the very least one should have that⊥..⊤ <:: *
. -
One could take the analogy to singleton types one step further and allow intervals
A .._K B
over kindsK
other than*
. E.g.(λx:A₁.B₁) .._(* → *) (λx:A₂.B₂)
would be an interval over unary type operators. Note the kind annotation to make sure the bounds of the interval are of the same kind. This is closer in spirit to the way abstract, higher-kinded type members are handled in dotty, where one can write e.g.
{ type F <: List }
(which the compiler η-expands to)
{ type F <: λX.List[X] }
While it is unclear whether this would simplify or complicate the meta theory, it would likely make the existing theory from systems with singleton types more easily applicable in the DOT setting.
Note that the more liberal, kind-annotated variant of intervals can be encoded in terms of the
*
-only variant. Again, this has already been noticed, for the case of singleton kinds, by Stone and Harper:2S .._* T = S..T F .._(x: S)→K G = (x: S) → (F x) .._K (G x)
-
This proposal originally contained the following two extra subtyping rules:
Γ, x: S ⊢ T₁ <: T₂ -------------------------- (T-λ-<:-λ) Γ ⊢ λx: S. T₁ <: λx: S. T₂ Γ ⊢ S₁ <: S₂ ---------------- (T-App-<:-App) Γ ⊢ S₁ t <: S₂ t
However, as Martin pointed out in a comment to his gist (https://gist.github.com/odersky/36aee4b7fe6716d1016ed37051caae95), these rules might not add any expressivity in practice. Consider the following example taken from his comment:
type C(x) <: Seq(x)
is encoded as
{ C :: (x: {A::*}) → ⊥..(Seq x) }
Then
p.C y :: ⊥..(Seq y)
Hence
p.C y <: Seq y
Although this idea does not seem to extend to the case of partial applications, e.g.
type Map[K, V] <: GenMap[K, V] Map Int <: GenMap Int ?
such partial applications can only occur nested inside other subtyping derivations but never directly in (T-Sub), (T-<:-..) or (T-..-<:) since partially applied types necessarily have arrow-kinds.
The following example illustrates that type safety does not hold for the proposed calculus (neither for the above version, nor for Martin's original proposal).
let x: { A :: { B :: x.A → ⊤..⊥ }..{ B :: x.A → ⊤..⊥ } } =
new(x: { A :: { B :: x.A → ⊤..⊥ }..{ B :: x.A → ⊤..⊥ } })
{ A = { B :: x.A → ⊤..⊥ } } in
let y: { B :: x.A → ⊤..⊥ } =
new(y: { B :: (z: x.A) → (z.B z)..(z.B z) })
{ B = λz: x.A. z.B z } in
let z: y.B y = () in
(z: ⊥)
To see that this example typechecks, let's first verify that the declared types of x
, y
and z
match the types of their definitions.
-
For
x
, we have thatx.A → ⊤..⊥
is a kind (syntactically), so we immediately get{ B :: x.A → ⊤..⊥ } :: *
by (K-{::}-F). From there, we get the declared type by applying the usual sequence of (K-..-I), (D-{::}), (T-{}-I) and (T-Unfold). -
For
y
, we need to show that(z: x.A) → (z.B z)..(z.B z) <:: (z: x.A) → ⊤..⊥
(note the absurd bounds on the codomain). LetΓ = x: { A :: { B :: x.A → ⊤..⊥ }..{ B :: x.A → ⊤..⊥ } }
andΓ′ = Γ, z: x.A
, then by (T-Var) and (K-Sel)Γ′ ⊢ x.A :: { B :: x.A → ⊤..⊥ }..{ B :: x.A → ⊤..⊥ }
by (T-Var), (T-<:-..) and (T-Sub)
Γ′ ⊢ z : { B :: x.A → ⊤..⊥ }
by (K-Sel)
Γ′ ⊢ z.B :: x.A → ⊤..⊥
by (T-Var) and (K-→-E)
Γ′ ⊢ z.B z :: ⊤..⊥
by (T-..-<:) and (T-<:-..)
Γ′ ⊢ ⊤ <: z.B z <: ⊥
by (K-..-<::-..) and (K-→-<::-→)
Γ ⊢ (z: x.A) → (z.B z)..(z.B z) <:: (z: x.A) → ⊤..⊥
-
For
z
, it's sufficient to show that⊤ <: y.B y
. LetΓ′′ = Γ, y: { B :: x.A → ⊤..⊥ }
, then by (T-Var) and (K-Sel)Γ′′ ⊢ y.B :: x.A → ⊤..⊥
by (T-Var), (K-Sel) and (T-..-<:)
Γ′′ ⊢ { B :: x.A → ⊤..⊥ } <: x.A
by (T-Var) and (T-Sub)
Γ′′ ⊢ y : x.A
by (T-Var) and (K-→-E)
Γ′′ ⊢ y.B y :: ⊤..⊥
by (T-..-<:) and (T-<:-..)
Γ′′ ⊢ ⊤ <: y.B y <: ⊥
It follows that y.B y
has absurd bounds in a context that corresponds to a store. Equivalently, we can substitute x
and y
by their definitions to obtain a closed type with absurd bounds. In either case, the type lattice becomes trivial.
The example is a variant of the well-know technique for typing arbitrary lambda terms in a system with (iso-)recursive types (see e.g. TAPL, ch. 20, pp. 273). Here, we lift this technique to the kind level to allow kinding arbitrary lambda expressions on the type level. Then we construct a divergent type expression and kind it with absurd bounds.
This unsoundness example makes crucial use of
- recursion in types (or rather in bounds of type members), and
- path-dependent type families.
The former is also present in Scala/dotty where as the latter is not. The example does therefore not constitute a soundness issue in those languages. Since this soundness issue is specific to HK DOT, it's worth elaborating a bit on this point. The different sorts of arrows in HK DOT (and Scala/dotty) can be categorized according to the sort of their domain and codomain:
-
(possibly path-dependent) function type (domain: type, codomain: type), inhabited by term-level lambdas/functions/methods,
example in DOT
f : (x: S) → T where S ≠ { A :: K } f = λx: S. t
examples in Scala/dotty
def f(x: S): T = t val g: (x: S) => T = (x: S) => t
-
universal quantifier/polymorphic type (domain: kind, codomain type), inhabited by polymorphic terms/functions
examples in DOT
f : (x: { A :: K }) → T f = λx: { A :: K }. t
examples in Scala/dotty
def f[X]: T = t def f[X[_]](y: ...): T = t
-
kind of path-indexed type families (domain: type, codomain: type), inhabited by type families or path-indexed singleton kinds
examples in HK DOT
F :: (x: S) → K where S ≠ { A :: K′ } F = λx: S. T
alternatively, using Martin's variant
F <: all(x: S)K where S ≠ { A : K′ } F = all(x: S)J J singleton, J <: K
there is no counterpart of this in Scala/dotty
-
kind of type operators, i.e. higher kind (domain: kind, codomain: kind), inhabited by type operators/functions/lambdas
examples in HK DOT
F :: (x: { A :: K′ }) → K F = λx: { A :: K′ }. T
in Martin's variant
F <: all(x: { A : K′ })K F = all(x: { A : K′ })J J singleton, J <: K
example in Scala/dotty
F[X] >: S <: T F[X, Y, Z] >: S <: T F[X[_]] >: S <: T F[X] = T
In other words, the kind language of both variants of HK DOT are strictly more expressive than that of Scala/dotty, which suggests that the soundness issue could be avoided by restricting kinds as follows:
K ::= (x: { A :: K }) → K′ type operator kind
S..T type interval kind
This restriction is purely syntactic and remains "compatible" with Scala/dotty in that any (higher-kinded) abstract type definition expressible in Scala can still be encoded in this subset.
- D. Aspinall, Subtyping with singleton types, CSL'94, LNCS 933, 2005. http://dx.doi.org/10.1007/BFb0022243
- C. A. Stone, R. Harper, Deciding Type Equivalence in a Language with Singleton Kinds, POPL '00. http://doi.acm.org/10.1145/325694.325724
- C. A. Stone, R. Harper, Extensional Equivalence and Singleton Types, ACM TCL 7(4), 2006. http://doi.acm.org/10.1145/1183278.1183281
- N. Amin, S. Grütter, M. Odersky, T. Rompf, S. Stucki, The Essence of Dependent Object Types, WadlerFest, LNCS 9600, 2016. http://dx.doi.org/10.1007/978-3-319-30936-1_14
- N. Amin et al., The DOT Calculus. Additional material including a detailed type safety proof with an accompanying Coq formalization. http://wadlerfest.namin.net/
I don't see how this would break things. Two types
p.A
andq.A
are equal whenp ≡ q
syntactically (as witnessed by (Refl)). So in particular, for any valuev
and typex.A
, sincex.A <: x.A
you also havev.A <: v.A
after substituting occurrences ofx
byv
in any (sub-)typing derivation.Actually, there is an issue in your example because the body of
a
is ill-typed. We havebut
x.A ≠ y.A
and the declared upper bound ofx.A
is⊤
so we can't up-castx.A
toy.A
. In fact,y.A
seems ill-formed, so there's probably something I'm misunderstanding about this example.Again, I don't understand the problem with your example. Maybe it will become more clear once we resolved the confusion about the first issue?
I haven't read your paper on F_{\Omega}^{\Mu*} yet but I assume that this requires reducing under fixpoint-operators? In DOT, we cannot just reduce under μs because they might make absurd assumptions (remember that preservation does not hold for open terms and types in DOT).
Also, note that
types in DOT are iso-recursive not equi-recursive: although the fold/unfold operations don't appear in the syntax, they definitely appear in typing derivations;
this problem is already present in Wadlerfest DOT where we don't have higher kinds, and it doesn't cause trouble, consider
it may not be necessary to normalize types to show soundness -- in fact, I very much hope it isn't.
If I understand your question correctly, you're asking whether there are infinite sequences of subtyping steps for such types (corresponding to an infinite sequence of reductions)? Let
p
be the path from my example, i.e.Note the very precise kind: my original example was actually ill-kinded! Now, let
int = new(_:_){ A = Int }
and considerp.F int
(i.e. the encoding ofF[Int]
), then we haveand so by (T-<:-..)
Similarly,
and so on.
I'm a bit worried that my observation about types not having normal forms is sending us on a wild-goose chase. I merely wanted to make the point that proof techniques for preservation that rely on normalizing types will probably not work in this case. Examples of such techniques seem common for Fω-like systems,4, 5, 6 so one might be tempted to apply them here.
Yes, this is part design, part notational laziness. We usually do assume that terms, types and kinds in judgments
Γ ⊢ J
are all well-scoped in the sense that all variables present inJ
are also given a type inΓ
. But this assumption is left implicit. On the other hand, we do not assume that types and kinds are well-formed, e.g. judgments likeΓ ⊢ λx:Int. λy:(x.A). y : (x: Int) → x.A → x.A
are derivable.Whooops, thanks for the corrections! :-)
Yes, I found that paper as well. I'm quite happy that you mention hereditary substitution, actually, because I think it will be key to solving the issues with the meta theory that I described, though not in the obvious way. I'll come back to that below.
That's not quite true. It is true that associating the arguments in the spine to the corresponding variables in open terms is part of the problem (or rather part of the solution) but that is only half the story. The crucial point is that the typings
p₁ : T₁
,p₂ : T₂
, ...,pₙ : Tₙ
of the arguments in the spine, need not be "strict", i.e. they might make arbitrary use of subsumption. Consequently, the domainT
of the kind(x: T) → U₁..U₂
ofS
need not have tight bounds. This is incompatible with tight subtypingΓ ⊢# S <: T
because the latter only allows type member selection on (strictly-typed) variables with tight bounds:consequently, we can not use tight subkinding in the second premise of the tight version of (K-→-<::-→):
because there is no guarantee that
T₂
has tight bounds (it most likely doesn't). As a consequence, we need to show that the following substitution lemma (or a generalization thereof) is admissible:Note that the conclusion uses tight sub-kinding, where as the first premise does not. So in order to prove this substitution lemma, we need to first show that the non-tight variants of (T-<:-..), (T-..-<:) are admissible in in tight subkinding derivations, which is exactly what we set out to prove in the first place.
Again, the problem is not so much the value of
x
in the store as it's typing: a derivation ofΓ ⊢# x : T₂
may make use of subsumption, which meansΓ, y: T₂
does not correspond to a stores[y := x]
. The definition of the "corresponds to a store" relations ~ Γ
requires all store locations to be typed strictly.I think what we need to solve this problem is something along the lines of hereditary substitution. Though, maybe surprisingly, not to normalize type expressions but to "normalize" subtyping derivations. Conceptually, hereditary substitution is re-normalizing terms after substitutions in order to eliminate any new redexes or "cuts" that might have been created. But this principle can be applied more generally in situations where one wants to maintain "cut-free" representations of derivations in the face of substitution. An example is algorithmic (sub-)typing for full F-<: as described in TAPL (ch. 28, p. 424): in this setting, uses of subsumption and transitivity corresponds to cuts/redexes and are "normalized" or "evaluated" away by the proof of their admissibility in algorithmic subtyping derivations. To do so one needs to simultaneously show that both transitivity and context narrowing are admissible in order to contract uses of the (SA-All) rule that relates ∀-types. The proof of context narrowing essentially performs a substitution of a subtyping derivation for a a bounded variable, followed by re-normalization of the result via transitivity. This pair of mutually recursive proofs thus has a structure reminiscent of that of hereditary substitution.
I believe that the same principle applies in this context although with more complicated "cuts" and rather non-standard "reductions". Essentially, the idea is to push uses of structural subtyping/-kinding rules as far down the derivation tree as possible (i.e. closer to the conclusion). But importantly, I'm not proposing that we try to normalize types themselves or eliminate all uses of transitivity. And even more importantly, we should normalize (sub-)typing derivations under non-store contexts.
For example, the following typing derivation
where
Γ(x) = { A: S₁..S₂ }
withS₁ ≠ S₂
, should be normalized asNote that a) the context
Γ
does not correspond to a store, and b) that the "normalized" derivation contains a use of transitivity that cannot be eliminated.The goal is to find a "normal form" for subtyping derivations that eliminates all uses of transitivity and non-structural subtyping rules in the empty context resp. in contexts that correspond to stores (i.e. for subtyping closed terms), so that preservation and canonical forms becomes essentially a matter of inverting structural (sub-)typing in such contexts.
Of course, all of this hinges on there actually being a suitable termination measure for this edifice of mutually recursive normalization/admissibility proofs, but that's where I believe thinking in terms of hereditary substitution may help.
I admit there are a lot of "if"s and "but"s and it's all still rather vague and abstract at this point. But at least it's a starting point...
As pointed out above, DOT doesn't use equirecursion: folding and unfolding is achieved through typing rules, not through subtyping rules.
References