@@ -11,6 +11,7 @@ The type system defines the following types:
11- Polymorphic Types
11- Polymorphic Types
12- Constrained Types
12- Constrained Types
13- Type Synonyms
13- Type Synonyms
15Primitive Types
16Primitive Types
16---------------
17---------------
@@ -68,24 +69,34 @@ A type annotation can also be provided::
68 identity :: forall a. a -> a
69 identity :: forall a. a -> a
69 identity x = x
70 identity x = x
71−Functions may also be polymorphic in row types or type variables with other kinds (see "Kind System")::
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").
77+For example, the following function accesses two properties on a record::
73 addProps o = o.foo + o.bar
79 addProps o = o.foo + o.bar
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
84+ forall r. { foo :: Number, bar :: Number | r } -> Number
86+Here, the type variable ``r`` has kind ``# *`` - it represents a `row` of `types`. It can be instantiated with any row of named types.
88+In other words, ``addProps`` accepts any record which has properties ``Foo`` and ``Bar``, and *any other record properties*.
77−So, the following compiles::
90+Therefore, the following application compiles::
79 addProps { foo: 1, bar: 2, baz: 3 }
92 addProps { foo: 1, bar: 2, baz: 3 }
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::
83 addProps { foo: 1 }
96 addProps { foo: 1 }
85since the `bar` property is missing.
98since the `bar` property is missing.
87−Again, a type annotation can be provided if necessary.
89Rank N Types
100Rank N Types
90------------
101------------
@@ -106,6 +117,23 @@ An argument to ``poly`` must indeed be polymorphic. For example, the following f
107since the skolemized type variable ``a`` does not unify with ``Number``.
118since the skolemized type variable ``a`` does not unify with ``Number``.
123+A row of types represents an unordered collection of named types without duplicates.
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.
127+To denote a closed row, separate the fields with commas, with each label separated from its type with a double colon::
129+ (name :: String, age :: Number)
131+It may be necessary, depending on the context, to surround a row in parentheses.
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::
135+ (name :: String, age :: Number | r)
109Type Synonyms
137Type Synonyms
110-------------
138-------------
@@ -129,14 +157,3 @@ Type Annotations
129Most types can be inferred (not including Rank N Types and constrained types), but annotations can optionally be provided using a double-colon::
157Most types can be inferred (not including Rank N Types and constrained types), but annotations can optionally be provided using a double-colon::
131 one = 1 :: Number
159 one = 1 :: Number
136−There are two primitive kinds, the kind ``*`` of types and the kind ``!`` of effects.
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.
140−Type constructors are given the arrow kind ``k1 -> k2`` for appropriate kinds ``k1``, ``k2``.
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.