sstucki/hk-dot-starwman.md Secret

## hk-dot-starwman.md

      
    Raw
  

              hk-dot-starwman.md
            
          
    DOT with higher-kinded types -- A sketch

Definitions

Syntax

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.
Reduction rules

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

Typing

Term typing

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

Definition typing

Γ ⊢ t : T
------------------------- (D-{:})
Γ ⊢ { a = t } : { a : T }

Γ ⊢ T :: K
-------------------------- (D-{::})
Γ ⊢ { A = T } : { A :: K }

Γ ⊢ d₁ : T₁     Γ ⊢ d₂ : T₂
--------------------------- (D-∧)
Γ ⊢ d₁ ∧ d₂ : T₁ ∧ T₂

Subtyping

---------- (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₂

Kinding

---------- (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₂

Sub-kinding

Γ ⊢ 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
types¹.  Type interval kinds can be
understood to be a generalization of singleton
kinds²: clearly, every singleton {T}_*
can be encoded as a singleton interval T..T.  Most of the
literature on the properties of systems with singleton types and
kinds seems to use PER-semantics^{1,
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 Harper², 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,¹
 Γ ⊢ M : A
 ------------- ({}-I)
 Γ ⊢ M : {M}_A

and Stone and Harper's introduction rule for singleton
kinds.²
 Γ ⊢ 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 kinds K 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:²
 S .._*        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.


Unsoundness

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 that x.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.
References


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/