◄ WORLD V · SONNY 5DART 258 · a helldive at the net

THE HIGHER-KINDED TYPE types have types — and they are called kinds

If values have types, then types have kinds. A plain type like Int has kind *. A type constructor like List is not a type until you apply it — it has kind * → * (give it a type, get a type). Pair has kind * → * → *. A higher-kinded type abstracts over these constructors, letting you write code polymorphic in the container, not just the element — Functor f, Monad m, one map for List and Maybe and Tree alike. Kinds are the type system's own type system, one level up.

THE TECHNIQUE kinds: Int : * ; List : *→* ; Pair : *→*→*

Kinds track the arity of a type constructor. The demo reads the kind arity of Pair (a two-argument constructor) and shows a partial application: live demo







  
HISTORY & CREDIT Girard (Fω) 1972 · Haskell

  
“Types are the top of the tower.” — there is another floor: kinds, the types of types. Without it you can be generic over elements; with it you can be generic over containers, and map stops being copy-pasted per data structure. cited

  
1972 · Jean-Yves Girard — System Fω: abstraction at the level of type constructors (kinds).
lineage · Barendregt's lambda cube places Fω on the “types depend on types” axis.
now · Haskell's Functor/Monad (kind *→*), Scala's higher-kinded generics.

  
Kinds are types one level up: they keep you from writing List Int Int (too many arguments) the way types keep you from 1 + true. The tower has more than one floor. Fω






  
RECOMMEND FOR I-13 kind arity + partial application, computed

  
On the canonical compiler, Pair has kind arity 2; the demo also computes a nested count 2ⁿ = 4 to exercise the arithmetic:

  
$ i13 run t_hkt.i13   # kind arities
list_kind = 1          -- List : * -> *
pair_kind = 2          -- Pair : * -> * -> *
nested = 4             -- 2^pair_kind, a sanity computation

  
Recommend: higher-kinded types are two levels above where i13 lives. i13 has no types (*), so it certainly has no kinds (the types of types). Being polymorphic over a container — one map for every Functor — requires the whole tower i13 declined to build. It computes kind arities as plain numbers (Pair = 2), but that is arithmetic about a system it does not implement. This is the clearest “far end” of the batch: the abstraction i13's f64-floor is furthest from.