Changes between Version 3 and Version 4 of RankNTypes


Ignore:
Timestamp:
Jan 6, 2006 11:22:22 AM (10 years ago)
Author:
ross@…
Comment:

some details

Legend:

Unmodified
Added
Removed
Modified
  • RankNTypes

    v3 v4  
    66== Brief Explanation ==
    77
    8 Haskell 98 provides only rank-1 types: universal quantification is over the whole type expressions, and is implicit, e.g.
     8In Haskell 98, all free variables in a type are implicitly universally quantified, e.g.
    99{{{
    1010const :: a -> b -> a
    1111}}}
    12 Rank-2 types may have polymorphic arguments, marked by `forall`, e.g.
     12Thus Haskell 98 permits only rank-1 types.
     13The 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
     19where ''monotype'' is a Haskell 98 type.
     20Note 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:
    1323{{{
    14 plus :: (forall a. a -> a) -> (forall a. a -> a) -> b -> b
     24succ :: (forall a. a -> a) -> (forall b. b -> b)
     25succ :: forall b. (forall a. a -> a) -> b -> b
    1526}}}
    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.
     27It is not possible to infer higher-rank types in general; type annotations must be supplied by the programmer in many cases.
    2728
    2829== References ==
    2930 * [http://www.haskell.org/ghc/docs/latest/html/users_guide/type-extensions.html#universal-quantification Arbitrary-rank polymorphism] in the GHC User's Guide.
    3031 * [http://research.microsoft.com/Users/simonpj/papers/higher-rank/index.htm Practical type inference for arbitrary-rank types], Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich and Mark Shields, July 2005.
     32 * [http://www.haskell.org/onlinereport/decls.html#type-semantics Semantics of Types and Classes] in the Haskell 98 Report
     33 * PolymorphicComponents would also be allowed higher-rank types
    3134 * [wiki:Rank2Types] are a special case
     35
     36== Details ==
     37
     38Hindley-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.
     39The 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.
     40A mixture of bottom-up inference and top-down checking often produces more informative error messages.
     41
     42For 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.
     43In 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
     48The 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
     51The 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.
    3255
    3356== Pros ==