@@ -11,6 +11,7 @@ The type system defines the following types:
1111- Polymorphic Types
1212- Constrained Types
1313- Type Synonyms
14+- Rows
1415
1516Primitive Types
1617---------------
@@ -68,24 +69,34 @@ A type annotation can also be provided::
6869 identity :: forall a. a -> a
6970 identity x = x
7071
71−Functions may also be polymorphic in row types or type variables with other kinds (see "Kind System")::
72+Row Polymorphism
73+----------------
74+
75+Polymorphism is not limited to abstracting over types. Values may also be polymorphic in types with other kinds, such as rows or effects (see "Kind System").
76+
77+For example, the following function accesses two properties on a record::
7278
7379 addProps o = o.foo + o.bar
7480
75−Here, `addProps` is inferred to have type ``forall r. { foo :: Number, bar :: Number | r } -> Number`.` That is, it can take any type which has properties ``Foo`` and ``Bar``, and *any other record properties*.
81+The inferred type of `addProps` is
82+
83+::
84+ forall r. { foo :: Number, bar :: Number | r } -> Number
85+
86+Here, the type variable ``r`` has kind ``# *`` - it represents a `row` of `types`. It can be instantiated with any row of named types.
7687
77−So, the following compiles::
88+In other words, ``addProps`` accepts any record which has properties ``Foo`` and ``Bar``, and *any other record properties*.
89+
90+Therefore, the following application compiles::
7891
7992 addProps { foo: 1, bar: 2, baz: 3 }
8093
81−but the following does not::
94+even though the type of ``addProps`` does not mention the property ``baz``. However, the following does not compile::
8295
8396 addProps { foo: 1 }
8497
8598since the `bar` property is missing.
8699
87−Again, a type annotation can be provided if necessary.
88−
89100Rank N Types
90101------------
91102
@@ -106,6 +117,23 @@ An argument to ``poly`` must indeed be polymorphic. For example, the following f
106117
107118since the skolemized type variable ``a`` does not unify with ``Number``.
108119
120+Rows
121+----
122+
123+A row of types represents an unordered collection of named types without duplicates.
124+
125+Rows have kind ``# k`` for some kind ``k``, and so values do not have types which are rows. Rather, rows can be used in type signatures to define record types or other type where labelled, unordered types are useful.
126+
127+To denote a closed row, separate the fields with commas, with each label separated from its type with a double colon::
128+
129+ (name :: String, age :: Number)
130+
131+It may be necessary, depending on the context, to surround a row in parentheses.
132+
133+To denote an open row (i.e. one which may unify with another row to add new fields), separate the specified terms from a row variable by a pipe::
134+
135+ (name :: String, age :: Number | r)
136+
109137Type Synonyms
110138-------------
111139
@@ -129,14 +157,3 @@ Type Annotations
129157Most types can be inferred (not including Rank N Types and constrained types), but annotations can optionally be provided using a double-colon::
130158
131159 one = 1 :: Number
132−
133−Kind System
134−-----------
135−
136−There are two primitive kinds, the kind ``*`` of types and the kind ``!`` of effects.
137−
138−For each kind ``k`` there is also a kind ``# k`` of rows, with types of kind ``k``. 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.
139−
140−Type constructors are given the arrow kind ``k1 -> k2`` for appropriate kinds ``k1``, ``k2``.
141−
142−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.