12 | | Rank-2 types may have polymorphic arguments, marked by `forall`, e.g. |
| 12 | Thus Haskell 98 permits only rank-1 types. |
| 13 | The proposal is to allow explicit universal quantification within types using a `forall` keyword, so types can have the forms |
| 14 | |
| 15 | * ''type'' `->` ''type'' |
| 16 | * `forall` ''vars''. [''context'' `=>`] ''type'' |
| 17 | * ''monotype'' |
| 18 | |
| 19 | where ''monotype'' is a Haskell 98 type. |
| 20 | Note that `forall`'s are not allowed inside type constructors other than `->`. |
| 21 | |
| 22 | `forall`s and contexts in the second argument of `->` may be floated out, e.g. the following types are equivalent: |
16 | | Rank-3 types may have arguments of rank-2 type, e.g. |
17 | | {{{ |
18 | | f3 :: ((forall a. a->a) -> Int) -> Bool -> Bool |
19 | | }}} |
20 | | and so on to arbitrary depth. |
21 | | |
22 | | `forall`s in the second argument of `->` could be permitted as a convenience, but they are equivalent to `forall`s further out. |
23 | | `forall`s are not permitted inside arguments of other type constructors. |
24 | | |
25 | | The GHC User's Guide has some vague remarks about how type signature information is used. |
26 | | Perhaps someone could elaborate. |
| 27 | It is not possible to infer higher-rank types in general; type annotations must be supplied by the programmer in many cases. |
| 35 | |
| 36 | == Details == |
| 37 | |
| 38 | Hindley-Milner type systems (e.g. in Haskell 98) may be specified by rules deriving the type of an expression from those of its constituents, providing a simple way to reason about the types of expressions. |
| 39 | The rules may also be used as a bottom-up procedure for inferring principal types, with inferred types matched against any signatures supplied, but many other traversals yield the same answer. |
| 40 | A mixture of bottom-up inference and top-down checking often produces more informative error messages. |
| 41 | |
| 42 | For arbitrary-rank types, a particular bidirectional traversal is specified by the type rules (see Fig. 8 on p25 of [http://research.microsoft.com/Users/simonpj/papers/higher-rank/index.htm the paper]), to make use of programmer-supplied annotations. |
| 43 | In particular, |
| 44 | * functions and expressions with type signatures are checked top-down. |
| 45 | * parameter variables without explicit signatures are assigned monotypes in upwards inference, but may inherit arbitrary-rank types in downwards checking. |
| 46 | * in an application (whether inferred or checked), the type of the function is inferred bottom-up, and the argument checked top-down against the inferred argument type. |
| 47 | |
| 48 | The generalization preorder must be recursively defined, with contravariance for `->` types (see Fig. 7 on p22 of |
| 49 | [http://research.microsoft.com/Users/simonpj/papers/higher-rank/index.htm the paper]). |
| 50 | |
| 51 | The system has the following properties: |
| 52 | * Programs containing no `forall`s are typeable if and only if they are typeable in Haskell 98. |
| 53 | * Inference produces principal types, though checking may accept more types. |
| 54 | * Both checking and inference are monotonic with respect to the generalization preorder. |