hkdot-vars.md

#DOT with higher-kinded types

A version of DOT with higher-kinded types that's based on the Wadlerfest formulation.

##Syntax

Var         x, y, z
Value          v, w ::= lambda(x:T)t
                        new(x:T)d
Term           s, t ::= x
                        v
                        x y               term application
                        x.a               term member selection
                        let x = s in t    let
Definition        d ::= { a = t }         term member
                        { A : K }         type member
                        d & d

RefType           R ::= x.A
                        R x
Type        S, T, U ::= R
                        Top               top
                        Bot               bottom
                        S & T             intersection
                        all(x:S)T         dependent function type
                        rec(x:T)          recursive record type
                        { a : T }         term member
                        { A : K }         type member

Kind              K ::= all(x:S)K         dependent function kind
                        S..T              type interval kind

Context           Γ ::= ∅                 empty
                        Γ, x: T           extension

Typing

###Term typing Γ ⊢ x: T

These are exactly as in original DOT.

                           x:T in Γ
                         -----------
                          Γ ⊢ x : T

                        Γ, x:T ⊢ t: U
               -------------------------------
                Γ ⊢ lambda(x:T)t : all(x: T)U

                        Γ, x: T ⊢ d: T
                     -------------------
                      Γ ⊢ new(x:T)d : T

                 Γ ⊢ x: all(z:T)U    Γ ⊢ y: T
                ------------------------------
                      Γ ⊢ x y : [z:=y]U

           Γ ⊢ t: T    Γ, x: T ⊢ u: U    x ∉ fv(U)
          -----------------------------------------
                    Γ ⊢ let x = t in u : U

                        Γ ⊢ x: {a: T}
                       ---------------
                         Γ ⊢ x.a : T

                           Γ ⊢ x: T
                      ------------------
                       Γ ⊢ x: rec(x: T)

                       Γ ⊢ x: rec(x: T)
                      ------------------
                           Γ ⊢ x: T

                     Γ ⊢ x: T    Γ ⊢ x: U
                   -----------------------
                         Γ ⊢ x: T & U

                    Γ ⊢ x: T    Γ ⊢ T <: U
                   ------------------------
                           Γ ⊢ x: U

###Definition typing Γ ⊢ d: T

The second rule is adapted, the other two are as in original DOT.

                          Γ ⊢ t : T
                    ----------------------
                     Γ ⊢ {a = t} : {a: T}

                         K singleton
                     -------------------
                      Γ ⊢ {A:K} : {A:K}

                   Γ ⊢ d1: T1    Γ ⊢ d2: T2
                  --------------------------
                    Γ ⊢ d1 & d2 : T1 & T2

Singleton-kindedness T singleton (new)

                        T..T singleton

                         K singleton
                    ---------------------
                     all(x:S)K singleton

Kinding Γ ⊢ R: K (new)

                        Γ ⊢ x: {A: K}
                       ---------------
                          Γ ⊢ x.A: K

                 Γ ⊢ R: all(x:S)K    Γ ⊢ y: S
               -------------------------------
                       Γ ⊢ R y: [x:=y]K

###Sub-kinding: Γ ⊢ K1 <: K2 (new)

                 Γ ⊢ S2 <: S1    Γ ⊢ T1 <: T2
                ------------------------------
                     Γ ⊢ S1..S2 <: T1..T2

              Γ ⊢ S2 <: S1   Γ, x: S2 ⊢ K1 <: K2
             ------------------------------------
                Γ ⊢ all(x:S1)K1 <: all(x:S2)K2

###Subtyping Γ ⊢ T1 <: T2

The rules are as in original DOT, except for the last three rules, which are straightforward adaptations.

                          Γ ⊢ T <: T

                   Γ ⊢ S <: T    Γ ⊢ T <: U
                  --------------------------
                          Γ ⊢ S <: U

                         Γ ⊢ T <: Top

                         Γ ⊢ Bot <: T

                        Γ ⊢ T & U <: T

                        Γ ⊢ T & U <: T

                   Γ ⊢ S <: T    Γ ⊢ S <: U
                  --------------------------
                        Γ ⊢ S <: T & U

             Γ ⊢ S2 <: S1    Γ, x: S2 ⊢ T1 <: T2
            -------------------------------------
                Γ ⊢ all(x:S1)T1 <: all(x:S2)T2

                        Γ ⊢ T1 <: T2
                    ---------------------
                     Γ ⊢ {a:T1} <: a:T2}

                        Γ ⊢ K1 <: K2
                    ----------------------
                     Γ ⊢ {A:K1} <: {A:K2}

                         Γ ⊢ R: S..T
                        -------------
                         Γ ⊢ S <: R

                         Γ ⊢ R: S..T
                        -------------
                         Γ ⊢ R <: T

One more point worth noting: the stratified version of the calculus would not allow definitions like these, which are valid Scala:

class T { this =>
    type Q = /* some OK recursive type using Q itself, e.g. */  { def head: Int; def tail: Q }
    type F[X <: Q] = /* some definition making use of the bound on X, e.g. */ { def toQ(x: X): Q }
}

because the kind of F would refer the the self-reference (Q = this.Q). I.e. the above definition is encoded as

new (z: ...)
    { Q :: { head: Int; tail: z.Q }..{ head: Int; tail: z.Q } } &
    { F :: all(x: {Bot..x.Q}){ toQ: x.X -> z.Q }..{ toQ: x.X -> z.Q } }

even if we substitute the definition of Q itself, the recursive reference in the negative position does not go away because that definition contains z.Q as well.

This is in contrast to the simple "fix" of just not allowing arrow kinds with unboxed domains, i.e. restricting kinds to K ::= T..T | all(x: {K}).K. According to that restriction, the above encoding is OK.