@@ -0,0 +1,21 @@
4+The kind system defines the following kinds:
6+- ``*``, the kind of types.
7+- ``!``, the kind of effects.
8+- Arrow kinds ``k1 -> k2``
14+The kind ``# k`` of rows is used to classify labelled, unordered collections of types of kind ``k``.
16+For example ``# *`` is the kind of rows of types, as used to define records, and ``# !`` is the kind of rows of effects, used to define the monad ``Eff`` of extensible effects.
21+A type variable can refer to not only a type or a row, but a type constructor, or row constructor etc., and type variables with those kinds can be bound inside a ``forall`` quantifier.