Lifting the "Self or associated type" constraint on existentials

Since no one else answered this...

A type's kind is its signature for creating new types. That is, the kind of type constructor specifies the kind(s) of its argument(s); the kind ★ is used for individual types.

A generic function type's rank is its signature for type instantiation. The following algorithm computes the rank of a type; for simplicity we assume all functions are curried. Rank 0 functions are not generic; Rank 1 functions have an outer ∀T introducing some type variable T; Rank n+1 functions are higher-order which receive a generic function of Rank n as their first parameter.

So, a higher-kinded type is nothing more than a type constructor. Usually, these come up in discussions about what types can supposit for a type variable; in most languages, type variables only range over types of kind ★. Easy enough.

A higher-rank type is higher-order function satisfying two conditions: first of all, it is generic already; additionally its argument, a function, is itself also generic (or likewise for its argument, if also function, and so on, for arbitrary levels of nesting). This second condition specifies a nested inner generic context that is in some sense independent of the outer generic context specified in the first condition. The upshot is not just that you can pass around generic functions — such as the polymorphic identity function forall a. a -> a or the polymorphic constant function forall a b. a -> b -> a — but you can use them as polymorphic functions in generic function bodies.

HTH.

5 Likes