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/
Let me answer for now just on
(RecSel)
. I have some other comments, but that's where I understand things best.Ah, very interesting—
(Refl)
itself is "problematic" then. Do you model the fact that type selection, in Scala and other calculi, depends on object identity not object equality? It seems not. Object identity can be modeled in small-step semantics without ANF, so why does this calculus not do that? That might be an acceptable simplifying assumption, maybe even a good one, but at least ML module people care a lot about the difference (and dealing with it properly tends to be pretty subtle), and I suspect Martin would care as well. In ML, this shows up in the semantics of functors (generative vs applicative). And at least, you'd have to be pretty explicit on this change.Just to be clear: In Scala, copying an expression that creates an object will create two distinct objects, whose abstract type members are treated as distinct. Otherwise you don't have path-dependent types but go into proper dependent types.
That's the essence of the question I was asking, though apparently this affects even the reflexivity rule. You're right about the example I used, I should have used
x.A
instead ofy.A
. However, as long as you have (Refl), that example will not break preservation.Concretely, in Scala, and the νObj, Wadlerfest and OOPSLA'16 calculi,
v1.T = v2.T
is only true (ifT
is abstract) ifv1
andv2
are not just equal objects, but the same object. That's enforced either through ANF or (in OOPSLA'16) by having rule(SelX)
rather than reflexivity. (SelX) restricts reflexivity tox.T <: x.T
, notv.T
.So in Scala something like this wouldn't typecheck:
In fact, that doesn't parse in Scala, but I have a semi-convincing encoding of something similar below. Alternatively, the broken example exhibits the same property more properly, since there
x.T
is defined to beInt
but then the definition is hidden.Alternatively, object creation is not treated as a pure expression but as an expression with side effects (where the side effect is "creating a new object"), so that syntactically equal expressions don't produce equal values. In fact, to model properly the fact that
new(x: T)d
has side effects, and to keep allowing unrestricted inlining of values, most would not treatnew(x: T)d
as a value (the generated memory addresses, on the other hand, are fine as values).Scala encoding of example above: