@@ -0,0 +1,21 @@
1+Kind System
2+===========
3+
4+The kind system defines the following kinds:
5+
6+- ``*``, the kind of types.
7+- ``!``, the kind of effects.
8+- Arrow kinds ``k1 -> k2``
9+- Row kinds ``# k``
10+
11+Row Kinds
12+---------
13+
14+The kind ``# k`` of rows is used to classify labelled, unordered collections of types of kind ``k``.
15+
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.
17+
18+Quantification
19+--------------
20+
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.