mmmodularity!

» by Scott Kilpatrick

A static type parameter T of the form `T extends U` can be instantiated with an intersection, union, arrow, or tuple type. The variable T ranges over all different types that are subtypes of U. We hope that if T is a static type parameter of some function then the arguments and context of a call to that function uniquely determine the actual type for T (statically).

However, if T is a static type parameter of the form `T kind U` then T can only be instantiated with trait types — i.e. those types whose declaration sites declare `kind U`. T could not be instantiated with a tuple or arrow type since the user does not declare these.

In my proposal I give a definition of function that produces a product group object. Suppose I have some value x of type (ZZ, ZZ) and want to square x within the product group formed by (ZZ, ZZ) using the `pow` function declared as

pow[\G implements Group[\...\] ...\](a: G, n: ZZ): G

Ideally the type (ZZ, ZZ) would instantiate the variable G and everything would work out. In the body of `pow` a reference to G’s identity element, `G.e`, usually refers to a meta member named `e` on the trait denoted by G. But here G is not a trait type, it’s a tuple type, so we certainly didn’t declare any member `e` on it. The body of the `productGroup` function, declared more or less as

productGroup[\E, F\](g: Group[\E\], h: Group[\F\]): Group[\(E, F)\],

contains an anonymous object that implements the group operations and identity element for the product group. When calling `pow(x, 2)` how can we use the definition of the product group (E, F) = (ZZ, ZZ) from that anonymous object?

The `productGroup` is really more like an ML-style functor that takes some modules and produces a new one. Alternatively, it’s like a constrained instance declaration in Haskell, like the following

instance Eq a => Eq [a] where
  (=) xs ys = ... element-wise equality check ...

If we made that anonymous product group object a top-level trait instead, with an inexpressible name like Group$Product, then the `pow` function could instantiate the variable G with the type Group$Product and references to `G.e` would check out just fine. The limitation does not stop at implementations on compound, non-trait types — consider one like the Haskell example in which we want to provide a group structure for the trait type List[\T\]. So, perhaps this necessitates some sort of anonymous implementation construct like Haskell’s `instance` or JavaGI’s `implementation`.