Changes between Version 10 and Version 11 of Rank2Types


Ignore:
Timestamp:
Feb 17, 2007 12:28:58 AM (8 years ago)
Author:
ross@…
Comment:

incorporate Iavor's correction on (2)

Legend:

Unmodified
Added
Removed
Modified
  • Rank2Types

    v10 v11  
    66Functions may have polymorphic arguments, subject to three restrictions: 
    77 
    8  * Such functions must have explicit type signatures, using `forall` to bind polymorphic type variables, e.g. 
    9    {{{ 
     8 1. Such functions must have explicit type signatures, using `forall` to bind polymorphic type variables, e.g. 
     9    {{{ 
    1010g :: (forall a. a -> a) -> (Bool, Char) 
    1111}}} 
    12  
    13  * In the definition of the function, polymorphic arguments must be matched on the left-hand side, and can only be matched by a variable or wildcard (`_`) pattern.  The variable then has the polymorphic type of the corresponding argument, e.g. 
    14    {{{ 
     12 2. In the definition of the function, polymorphic arguments must be matched on the left-hand side, and can only be matched by a variable or wildcard (`_`) pattern.  The variable then has the polymorphic type of the corresponding argument, e.g. 
     13    {{{ 
    1514g f = (f True, f 'a') 
    1615}}} 
    17  
    18  * When such a function is used, it must be applied to at least as many arguments to include the polymorphic ones (so it's a good idea to put those first).  Each expression must have a generalized type at least as general as that declared for the corresponding argument, e.g. 
    19    {{{ 
     16 3. When such a function is used, it must be applied to at least as many arguments to include the polymorphic ones (so it's a good idea to put those first).  Each expression must have a generalized type at least as general as that declared for the corresponding argument, e.g. 
     17    {{{ 
    2018g id 
    2119g undefined 
    2220}}} 
    23 The more general [wiki:RankNTypes] remove the last two restrictions. 
    24  
    25 '''Questions from Iavor:''' 
    26  * The restriction that polymorphic arguments have to be matched by variable or wildcard (`_`) patterns does not appear to be specific to rank-2 types---it seems like an orthogonal decision. 
    27  * While the rank-N proposal removes restriction (3), in many cases the results may be unexpected.  For example, consider the classic example of using {{{runST}}}: 
    28 {{{ 
    29 x = runST (return a)     -- OK 
    30 y = runST $ return 'a'    
    31 }}} 
    32  The rank-2 design rejects {{{y}}} because {{{runST}}} needs an extra argument.  The rank-N design accepts this use but later fails because the inferred type for '{{{runST}}}' is 'less polymorphic  than expected'. 
    33  
    34  
    35  
    36  
    37  
    38  
     21The more general [wiki:RankNTypes] remove the last restriction in many cases. 
    3922 
    4023== References ==