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/
Agreed then. I assumed you'd know this but was surprised you didn't mention it—but Martin knew what you meant by "not using ANF".
Oh. I thought OOPSLA had values in the path language without full (Refl), but I was confused.
Let me try to focus my speculations on real problems then:
Map Int <: GenMap Int
and hereditary substitution.Well, what if I try to encode
def f[K <: GenMap Int] = ...; f[Map Int]
? In fact, it seems I currently won't needMap Int <: GenMap Int
, butMap Int <: λ x :: *. GenMap Int x
, and inspecting your subtyping rules suggests that's unprovable. No rule is applicable except transitivity (which defers the problem) or(T-<:-..)
and(T-..-<:)
(which don't apply at kind* -> *
).The reason is that encoding
K <: GenMap Int
requires an interval of non-* kind, which must be currently encoded using eta-expansion. However, type definitions (inf's
argument) need not be eta-expanded. Maybe(D-{::})
should be modified and force eta-expanded definitions, like (apparently) Dotty seems to do internally? Or maybe the rules should just be extended to handle this case somehow—right now, it seems I can't even proveF <: λ x :: *. F x
or viceversa.BTW, an algorithmic for
Map Int <: λ x. GenMap Int x
might need kind-directed eta-expansion, which is sort-of obvious but I've never heard. I have seen eta-expansion for equivalence checking (ATTAPL Ch. 6), but not for subtyping (though it can arise the same way). Of course google disagrees and points me to https://www.researchgate.net/publication/221557946_Syntactic_Metatheory_of_Higher-Order_Subtyping (which also uses HSubst, though on types, and mentions the barrier below).==
Great, you have a research problem and an attack!
I wondered about step-indexing here: it would allow the mutual recursion to proceed, but it wouldn't ensure the whole process terminates, so it's clearly not enough by itself...
Hereditary substitution (HSubst) might be a cool inspiration. This suggests maybe the best idea of this comment: have you tried adding proof terms to the subtyping rules, and phrasing reduction rules for those? That's maybe just notation, but it might help all those that get beta-reduction better than cut-elimination. (In fact, we even get to look informally at the "untyped" reduction rules if we want, though we probably shouldn't formalize those). The result might be of interest beyond Scala!
To this end, though, you might need to internalize dependency into assumptions using a term-level lambda, so that you can exhibit
(λ x: S. < proof term > : T <: U): (∀ x: S. T <: U)
. But that would probably complicate things...Then, can you explain the "leftover" transitivity/subsumption in a way similar to variables (and spines) in neutral terms?
Back to hereditary substitution: It does prove (weak? strong?) normalization for STLC ("Hereditary Substitutions for Simple Types, Formalized" details how) without logical relations.
But HSubst has limited power, though it might be enough: since (IIUC) hereditary substitution can be formalized in Peano Arithmetic, and since proves strong normalization (hence, with a few provisos consistency) of the object language, hereditary substitution alone can't work for type systems that extend Peano Arithmetic, such as System T, or System F (which proves second-order Peano Arithmetic consistent). I have no clue where the system you have sits, but maybe it's too powerful? But subtyping proofs don't have lambdas and subtyping lacks internalized implication, and maybe it can't be encoded suitably and this is all irrelevant.
There you need reducibility candidates or logical relations, which go beyond Peano Arithmetic. This point is made in "Proofs and Types", in the intros of Chapter 6 and 15, though I don't fully get all those intros. I've just seen it again mentioned in http://www.twelf.org/slr/.
Proofs and Types also doesn't actually mention hereditary substitution (it hints at "proof theoretic techniques" and I guess that's what they mean) or logical relations (but it mentions Tate '67).
If the barrier applies, it would suggest considering logical relations for transitivity elimination, but I've never heard of those. Parroting termination of STLC/System F, they'd be like "this subtyping proof is itself normalizing, and even the result of applying it to an assumption normalizes". What's confusing is that the property, it seems, would not be defined by induction on some "proof type", since you don't have internal abstraction on assumptions (unless you add lambdas, as sketched above), but by induction on the context. That's not novel though: logical relations are defined on closed terms usually, but they can be extended to open ones, and PFPL's chapter on "Equational Reasoning for T" (either edition) does exactly that, by defining open logical equivalence.