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

Hi Sandro,

Great work with the unsoundness example! The thing that strikes me is that it seems to rely on the fact that in the definition of x, x occurs again as a path of a parameter of some of the kinds that make up the definition of x. Maybe we can prevent that "knot"
by enforcing a stratification? What about we change the typing rule for new to:

             G, x: T |- d: T    T x-stratified
              ---------------------------------
                  G |- new(x: T): rec(x: T)

Here, T x-stratified means that for any kind of the form all(y: S)K appearing in some part of T we have x not in fv(S). The details how to express this in typing rules are a bit messy and involved. On the other hand, I don't think this would seriously cut down on expressiveness. WDYT?

I think the stratification you propose should indeed eliminate counterexamples like the one I found. That strategy reminds me of the "strict positivity" restrictions for inductively defined data types in languages like Agda. These are also meant to exclude Russel-type paradoxes like the one I use in the counterexample.

I think for a start it might be good to prove safety in a simplified calculus without explicit recursion (e.g. like D-<:). Even in a calculus like that, subtyping is already quite powerful, so proving safety is hard. The reason is a sort of "impredicativity" in DOT which makes it hard to find good induction measures when showing that substitution is admissible in a restricted subtyping judgment (such as "tight subtyping" in WF DOT). See this comment for details.

Another way of seeing this is that recursion/non-termination is sometimes "encodable" even in typed lambda calculi without an explicit fixpoint combinator in types/terms, provided they allow some universe/type/kind to contain itself (e.g. Type:Type). Unfortunately, finding counter examples based on such Girard-type paradoxes is much harder. (Thanks @Blaisorblade for noting the different roles of Russel vs. Girard-type paradoxes in this context.)

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.