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/
No, this calculus does not distinguish between object identity and object equality. BUT, the answer to your question really depends on what you mean by "object equality" and "object identity". In particular, types in this calculus are still path-dependent (as opposed to fully dependent) and the distinction between applicative and generative functors does manifest itself. I will go into some detail below as to why I think this is the case. But first, I'd like to clarify the essential difference between this calculus (or rather the first-order fragment) and that described in the Wadlerfest paper (WF-DOT).
Unlike WF-DOT, this calculus follows the tradition of typed lambda calculi (and various extensions thereof) in that it is referentially transparent in the sense that any definition can be replaced by its value (via substitution) without changing the overall result of the program. In STLC, for example, the two programs
(λx:T. f x x) λz:U.z
andf (λz:U.z) (λz:U.z)
yield the same result, and nobody would argue thatx
is a store location initialized byλz:U.z
or that, in copying the expressionλz:U.z
twice, we have somehow created distinct values. Expressions (and values in particular) are considered identical if they are syntactically equal. Depending on the calculus in question, this might be further relaxed to identify β/η-equivalent expressions. Whether or not this is an appropriate "design decision" for a calculus that deals with "objects" is a different question, which I'm not going to address here (though I will argue that it has some practical advantages below). Be that as it may, a direct consequence of this "design decision" is that the path language (represented by the syntactic categoryp
) has to be extended to also contain values (denoted byv
). This is because paths can appear in types in the form of type member selectionsp.A
: ifx.A
is a valid type expression, and we are serious about referential transparency, thenx.A[x := v] = v.A
must be a valid type expression as well.In other words, the problem (if any) is not with the (Refl) rule but with the choice to include values in the path language.
Note that despite the added flexibility, important restrictions remain.
Paths are still a subset of terms, in particular,
(u v).A
is not a path, nor isv.a.A
. As a consequence, types remain path-dependent (albeit for a more relaxed notion of "paths").A pair of type selections
v.A
andu.A
are comparable only if the valuesv
andu
are syntactically equal, no β/η-reductions are allowed,({a = λx.(λy.y)x} ∧ {A = ⊤}).A
and({a = λx.x} ∧ {A = ⊤}).A
are different.Indeed, he does. I have had many discussion with Martin about whether this is the right approach to formalizing Scala, and at present, we mostly agree that it essentially depends on how the calculus is to be used.
If you're interested in modeling Scala closely -- what happens in the compiler or at runtime -- then a WF-DOT, ANF-based, small-step formalization or an environment-based, OOPSLA'16-style, big-step formalization is probably what you want. In these calculi, variable names correspond to store/environment locations reflecting the familiar distinction between object identity and equality.
If you're interested in the more logical/type-theoretic aspects of the calculus, and about relating it (and its meta theory) to other typed lambda calculi, then a small-step formalization permitting substitutions in terms as well as in types is probably better suited. For example, developing a proof that an ANF-based WF-DOT simulates a substitution-based F-<: is a pain (in fact we don't have any such proof), whereas proving the simulation for a substitution-based variant of DOT is almost trivial (Nada mechanized it in Coq a while back).
In the end, I don't think either of the two approaches yields fundamental insights that cannot be gained from the other. On the contrary, I believe that switching between the two perspectives is more likely to reveal which features of the type system (and its meta theory) are accidental and which reflect deeper principles.
Functors remain generative in DOT, irrespective of the formalization. Remember that types are still path-dependent, so expressions of the form
(f x).A
are not allowed:f x
needs to be let-bound, at which point different instances can no longer be identified. ConsiderIn fact, this simpler example already fails in both calculi:
In fact, even if we changed the last line to
it would still not type check. Only if we consistently replace
x
by it's value do we get a typable program:I don't want to belabor this point unnecessarily, so I'm going to skip the remainder of your comments about object identity in Scala and other DOT versions vs. this one. But please let me know if any of the above remains unclear or dubious to you.
The extension of (T-..-<:) and (T-<:-..) to arrow-kinds is possible in principle but it requires the use of intervals over kinds other than
*
-- though these are readily encodable (as explained in the gist).A more interesting question, IMO, is how you would ever use the fact that
Map Int <: GenMap Int
, other than to show thatMap Int T <: GenMap Int T
, which is already covered by the current (T-..-<:) and (T-<:-..) rules.Yes, indeed, the same holds for the (K-→-<:-→) and (T-→-<:-→) rules, which, in combination with singleton types, already allows "reductions" under a binder. You are right that the resulting subtyping/-kinding relations can be absurd, but they do not constitute a soundness issue since they cannot escape the binder.
Yes, as mentioned in the gist, Harper and Stone already describe this in their papers on singleton types and kinds,2, 3 though I have not read the relevant chapter in PFPL. I should probably have a look at that.