Higher kinds are sexier

In the process of formalizing generics for my Lisp, I'm also studying FGJ_ω again, the extension of Featherweight Generic Java with higher kinds. Instead of just parameterizing types with first-order types, such as T, you can parameterize types with type-level "functions", such as F<T>. One example of such a function is the type List<T> - you give it a T, and it "returns" the concrete type of lists containing that type.

And it turns out, the theory behind that looks simpler, and thus sexier:

(types)             T ::= (K K*)
(type constructors) K ::= X | C | (P* => T)
(type param defs)   P ::= (X P*) | (<: (X P*) (C K*))
(class defs)        D ::= DEFCLASS (C P*) ((C K*)*)
(method defs)       M ::= DEFMETHOD (m P*) ((param T)* -> T)

I like the definition of types: a type's the application of a constructor to zero or more other constructors. Constructors may be variables (X), classes (C), or functions taking zero or more parameters and returning a type. (So you basically have a lambda calculus at the type-level.) A type parameter is a variable constructor with zero or more parameters, optionally bounded to a class type with zero or more type arguments. Class definitions are parameterized over zero or more type parameters, and extend zero or more existing classes. (I'm taking some liberties with adding multiple inheritance, hoping it doesn't mess up the theory. :P) Method definitions are, as usual, parameterized on the type- and term-level and have a result type.

It's kinda embarrassing to post this stuff here, since I'm so bad at type theory, but I think I can make it work. One insight giving me this faith is that none of this stuff survives till runtime: at runtime, only concrete instantiations, such as List<String> remain. Or so I hope.