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.

Formalizing generics

In the previous post, Minimal generics for an untyped language, I've discussed some basic requirements for the implementation of parametric polymorphism in the Lisp I'm working on.

I've now made some progress in formalizing this, based on Featherweight Generic Java. Here's a basic overview of the type system in the FGJ style:

(types)       T ::= C | X | Top
(classes)     C ::= (klass T*)
(class defs)  D ::= DEFCLASS (klass (<: X C)*) (C*) ((slot T)*)
(method defs) M ::= DEFMETHOD (method (<: X C)*) ((param T)* -> T)

Types are either class types (C), type parameters (X), or Top. Class types have a name (klass) and zero or more types as parameters. A class definition introduces a named class, parameterized over zero or more type parameters that have class types as bounds, zero or more superclass types, and zero or more named and typed slots. A method definition introduces a named method, parameterized over zero or more type parameters that have class types as bounds, with zero or more named and typed parameters and a result type.

Type parameters in a class definition or method definition (X) are scoped over the entire definition, including the bounds (in the style of F-bounded polymorphism).

All of this is pretty much equivalent to FGJ. The only difference is that classes do not contain methods.

[Updates: I've added type parameterization to method definitions. Added Top. Added some parentheses to make the syntax unambiguous.]

Minimal generics for an untyped language

So, I'm developing a Lisp, which means I have to support untyped, dynamically type-checked code in any case. But I still like typeful programming.

Generics, or parametric polymorphism, are jolly useful, even on a totally limited scale: all I want from the first round of this endeavor is to support something like the following:

(defclass (list T))
(defmethod add ((list (list T)) (element T))
...)

Here, I define the class (list T) - a list parameterized over the type of its elements, T. That's the same as Java's List<T>. The method ADD takes such a list and an element, and adds it to the list.

To create an instance of a parameterized class, you have to pass a concrete type argument to use for the element type, as in:

(defvar *my-list* (make (list string)))

This creates a list that accepts strings (and instances of subclasses of string) as elements.

The instance has to remember that it's a list of strings for type safety. When ADD is called on a list, the runtime needs to check that the element type matches:

(add *my-list* "foo") ;; OK
(add *my-list* 12) ;; runtime error

One more thing I'd also like is the following;

(defclass (foo (<: X bar)))

That's a class foo that has one parameter, that must be a subtype of bar, analogous to Java's Foo<X extends Bar>. Being able to give such a bound to a type parameter seems quite essential.

Furthermore, it has to be possible to pass on type parameters to superclasses, as in:

(defclass (super-1 T))
(defclass (super-2 T))
(defclass (klass X Y) ((super-1 X) (super-2 Y)))

(klass X Y) is parameterized over two types, X and Y, and passes them on to its two superclasses, each of which is parameterized over one type.

Of course, it also has to be possible to remove parameterization, as in:

(defclass string-list ((list string)))

This defines an unparameterized class string-list, which is a subclass of (list string).

Another requirement is that it has to be possible to create instances of type arguments, as in:

(defclass (klass T))
(defmethod make-a-new-t ((k (klass T)))
(make T))

That's just cute, and may have some applications to dependency injection.

I'd also like to be able to write polymorphic functions:

(defun identity ((a T) -> T) a)

The arrow indicates the result type of the function. In this case it takes an instance of any type and returns it.

It should also be possible to give slots (member variables) of classes the types of type parameters:

(defclass (klass X Y) ()
((slot-1 X)
(slot-2 Y)))

This defines a class with two type parameters X and Y, (no superclasses,) and two slots slot-1 and slot-2 with the types X and Y, respectively.

These are the basic requirements. Now I need a plan! ;)