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

In fact we do not need the rule

  G |- R1 <: R2
----------------
G |- R1 x <: R2 x

We can already express what we need with the other rules. Example:

type C(x) <: Seq(x)

is encoded as

C: all(x)Bot..Seq(x)

Then

C(y): Bot..Seq(y)

Hence

C(y) <: Seq(y)

With that simplification it looks like the meta-theory should be a relatively straightforward adaptation of the original proof. What do people think?

I think you are right in that we don't need the subtyping rule for fully applied type operators. I'm not sure there's a workaround for partial applications though, e.g.

type Map[K, V] <: GenMap[K, V]
Map Int  <:  GenMap Int   ?

I think this case might crop up in the meta theory, but I'm not sure.

Meta theory

As for the meta theory being a "straightforward adaptation of the original proof", I'm afraid that's not the case. Here's why.

Recall that the original proof relies on a "tightened" subtyping judgment, Γ ⊢# S <: T with more stringent subtyping rules for type selections:

Γ ⊢! x: {A: T..T}         Γ ⊢! x: {A: T..T}
-----------------         -----------------
Γ ⊢# T <: x.A             Γ ⊢# x.A <: T

where ⊢! denotes strict typing, which only allows very limited use of subsumption. The original rules are then shown to be admissible in typing contexts Γ that correspond to stores. The admissibility proof makes essential use of the "has-member" judgment, which is used to "unzip"/"invert" typings of the form Γ ⊢# x: {A: S..T} into Γ ⊢! x: {A: U..U} and Γ ⊢# S <: U, U <: T. The requirement that Γ correspond to a store is crucial because otherwise we might be in a situation where Γ, x: {A: S..T} ⊢# x: {A: S..T} and the interval S..T cannot be "unzipped" further.

In the presence of HK types, we might want to introduce a similar tight subtyping judgment where only

Γ ⊢! S :: T..T         Γ ⊢! S :: T..T
-----------------      --------------
Γ ⊢# T <: S            Γ ⊢# S <: T

are allowed, and a similar "has-member" (or rather "is-interval") judgment for types. However, things quickly get complicated. Firstly, the premise of the above rules might be derived as

Γ ⊢! x : {A: T..T}
------------------
Γ ⊢! x.A :: T..T

so one needs mutually inductively defined "has-member" judgments for both terms and types. Secondly, the judgment for types also needs to handle application, i.e. we need one or more rules

          ???
------------------------
Γ ⊢# S x :: K has U₁..U₂

Whatever the precise formulation of these rules, they will have to deal with the fact that S might have been kinded as

                            Γ, y: T₂ ⊢# K <:: U₁..U₂    ...
                            ------------------------------- (∀-<::-∀)
Γ ⊢# S :: ∀(y: T₁)K         ...
---------------------------------------- (K-Sub)
Γ ⊢# S :: ∀(y: T₂)U₁..U₂

Note that

1. we can't apply the usual "has-member"/"is-interval" lemmas here because the kind of S is not an interval, and
2. even with an additional "is-arrow" judgment, we still eventually need to unzip the subkinding relationship at the top of the above derivation, where, crucially, the environment doesn't correspond to a store any longer (due to the additional y: T₂).

This situation is reminiscent of the trouble caused by the presence of a subtyping rule for recursive types in DOT. However, unlike that rule, the (∀-<::-∀) subkinding rule is crucial in this calculus. Without it, we can't type e.g.

{ type F = List } <: { type F <: Seq }

I'm currently looking into possible solutions to this issue. Ideas are welcome.

Other issues

There are a number of issues with the above proposal which I tried to address in the updated/extended version (see https://gist.github.com/sstucki/3fa46d2c4ce6f54dc61c3d33fc898098). Here's a short discussion of these issues:

ANF in types

Just as Wadlerfest DOT, this proposal uses ANF throughout. I don't think this is helpful. At the very least, it requires let binders in types, since type-level computations need to be "boxed" and bound to term variables before they can be used in type applications. E.g. the following HK type definitions, can't be encoded using ANF without the use of type-level let binders:

type F[X] = List[List[X]]
type G[X] = List[X => X]

The intuitive encodings don't work because type applications of the form R1 (R2 x) are not permitted syntactically. We also can't bind the inner applications to helper variables outside of the definitions since they depend on the X parameter bound in the abstraction.

I think introducing let binders (along with corresponding kinding and subtyping rules) would unnecessarily complicate the calculus. Let's just not use ANF.

Type-level lambdas vs. singleton kinds

This is not so much an issue as a clarification: in my extended proposal I suggest to use type-level lambdas to initialize arrow/forall-kinds, e.g.

        λ(x: T)U :: ∀(x: T)U..U
---------------------------------------
{ A = λ(x: T)U } : { A :: ∀(x: T)U..U }

This is consistent with the way term-level lambdas inhabit arrow types and with the literature on HK types. You seem to prefer the use of singleton arrow-kinds and subkinding instead, e.g.

        ∀(x: T)U..U <:: ∀(x: T)U..U
--------------------------------------------
{ A :: ∀(x: T)U..U } <: { A :: ∀(x: T)U..U }

which is probably closer to what happens in the compiler? Of course, lambdas are still there, they are just disguised as singleton kinds now:

λ(x: T)U..U   ≡   { A :: ∀(x: T)U..U }.A

So I'm perfectly happy with either proposal, just as long as it doesn't complicate the meta theory.

To simplify the exposition, I'd treat singleton kinds syntactically (rather than through a separate judgment). I.e.

J  ::=  T..T  |  ∀(x: T)J

Kinding of non-RefTypes

Probably the biggest source of extra rules in my extended proposal comes from the fact that it gives kinds to all types.

You make a syntactic distinction between Types and RefTypes, and only RefTypes are kinded. I find that rather odd, could you maybe elaborate a bit on that? Why would you have types that are unkinded?

In any case, it leads to rather absurd results. Since RefTypes are included in Types, R..R is an OK singleton kind, which means any RefType R, irrespective of its actual kind can be treated as if it had kind R..R and thus (by subsumption) ⊥..⊤. This means we can encode and type-check definitions like

type A     = List => List
type F[X]  = X[X]
type Omega = F[F]

I don't know whether this constitutes a soundness issue or not, but it certainly seems strange.

The best solution I could come up with is to assign to every "proper" type T its singleton kind T..T, at the expense of eight additional kinding rules (one for each non-RefType plus one for lambdas). Obviously, I'm open for suggestions on how this could be simplified.

Minor issues

The type in the conclusion of the typing rule for recursive records is wrong (x might be free in T). It should be

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

The typing rule for let binders is missing:

        G |- t: T    G, x: T |- u: U    x not in FV(U)
        ----------------------------------------------
                   G |- let x = t in u : U

The subsumption rule for kinding is also missing:

                G |- T : K1    G |- K1 <: K2
                ----------------------------
                         G |- T : K2

The following is a translation of the safety counter example from my Gist to the syntax and statics described above. It illustrates that type safety holds for neither of the proposed HK DOT variants.

let x: { A : { B : all(z: x.A)Top..Bot }..{ B : all(z: x.A)Top..Bot } } =
    new(x: { A : { B : all(z: x.A)Top..Bot }..{ B : all(z: x.A)Top..Bot } })
           { A : { B : all(z: x.A)Top..Bot }..{ B : all(z: x.A)Top..Bot } } in
let y: { B : all(z: x.A)Top..Bot } =
    new(y: { B : all(z: x.A) (z.B z)..(z.B z) })
           { B : all(z: x.A) (z.B z)..(z.B z) } in
let z: y.B y = () in
(z: Bot)

Note. The type annotations/ascriptions on all the let-bound variables are just to indicate hidden uses of subsumption and could be removed.

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 { B :: all(z: x.A)Top..Bot } is a type (syntactically), so we immediately get { B :: all(z: x.A)Top..Bot }..{ B :: all(z: x.A)Top..Bot } as a singleton kind. From there, we get the declared type by applying the usual sequence of definition typing, Rec-introduction and unfolding.

• For y, we first apply definition typing, Rec-intro and unfolding. Next, we need to show that all(z: x.A) (z.B z)..(z.B z) <: all(z: x.A) Top..Bot as arrow kinds (note the absurd bounds on the codomain of the latter). Let Γ = x: { A : { B : all(z: x.A)Top..Bot }..{ B : all(z: x.A)Top..Bot } } and Γ′ = Γ, z: x.A, then by variable typing and kinding of type selections

   Γ′ ⊢ x.A : { B : all(z: x.A)Top..Bot }..{ B : all(z: x.A)Top..Bot }
  

  by variable typing and subsumption to the upper bound of x.A

   Γ′ ⊢ z : { B : all(z: x.A)Top..Bot }
  

  by kinding of type selections

   Γ′ ⊢ z.B : all(z: x.A)Top..Bot
  

  by variable typing and kinding of type applications

   Γ′ ⊢ z.B z : Top..Bot
  

  giving us the following bounds for z.B z

   Γ′ ⊢ Top <: z.B z <: Bot
  

  by subkinding of type intervals and arrow kinds

   Γ ⊢ all(z: x.A) (z.B z)..(z.B z) <: all(z: x.A) Top..Bot
  

  by subtyping of type members

   Γ ⊢ { B : all(z: x.A) (z.B z)..(z.B z) } <: { B : all(z: x.A) Top..Bot }
  

• For z, it's sufficient to show that Top <: y.B y. Let Γ′′ = Γ, y: { B : all(z: x.A)Top..Bot }, then by variable typing (of y) and kinding of type selections

   Γ′′ ⊢ y.B : all(z: x.A)Top..Bot
  

  by variable typing (of x), kinding of type selections and projecting the lower bound of x.A

   Γ′′ ⊢ { B : all(z: x.A)Top..Bot } <: x.A
  

  by variable typing (of y) and subsumption

   Γ′′ ⊢ y : x.A
  

  by kinding of type applications

   Γ′′ ⊢ y.B y :: Top..Bot
  

  giving us the following bounds for y.B y

   Γ′′ ⊢ Top <: y.B y <: Bot
  

In other words, y.B y has absurd bounds in a context that corresponds to a store and the type lattice collapses to the trivial relation.

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.