Changes between Version 10 and Version 11 of Ticket #57


Ignore:
Timestamp:
Apr 4, 2007 10:34:29 PM (7 years ago)
Author:
diatchki
Comment:

Moved the interesting bits to the page on PolymorphicComponents.

Legend:

Unmodified
Added
Removed
Modified
  • Ticket #57 – Description

    v10 v11  
    11see PolymorphicComponents. 
    2  
    3 These are some rough and unfinished  notes about the details of 
    4 adding polymorphic components to datatypes. 
    5  
    6 == Notation == 
    7  
    8 We need a notation to write the type schemes for polymorphic components. 
    9 Hugs and GHC differ slightly in their choice of notation. 
    10  
    11  
    12 === Recognizing Schemes === 
    13  
    14 We use 'forall' To indicate that a field in a constructor of a 
    15 'data' or a 'newtype' declaration is polymorphic. 
    16 In Hugs, 'forall' is implemented as a new keyword, while in GHC it 
    17 is a "special" identifier that is treated differently in contexts 
    18 that expect a type and in contexts that expect values.  For example, 
    19 the following definitions is rejected by Hugs but accepted by GHC: 
    20 {{{ 
    21 f forall = forall 
    22 }}} 
    23 PROPOSAL: adopt GHC's convention and treat 'forall' specially in 
    24 types but allow it to be used in value declarations. 
    25  
    26  
    27 === Notation for Schemes === 
    28  
    29 {{{ 
    30 scheme    = 'forall' tvars '.' opt_ctxt type 
    31  
    32 opt_ctxt  = context '=>' 
    33           | 
    34 }}} 
    35  
    36 The non-terminal 'tvars' is a sequence of type variables that are 
    37 separated by blank spaces.   We have a choice if we should allow 
    38 empty quantifier sequences. 
    39  
    40 ==== Some static checking ==== 
    41 Here are some differences between Hugs and GHC: 
    42  
    43 Hugs: 
    44   * does not allow empty quantifier lists 
    45   * requires that variables are mentioned in the body of a type 
    46   * permits predicates that do not mention any of the quantified variables 
    47  
    48 GHC: 
    49   * allows empty quantifiers 
    50   * warns when quantified variables are not mentioned the body of a type 
    51   * disallows predicates that do not mention any of the quantified variables 
    52  
    53 PROPOSAL: be liberal: 
    54   * allow empty quantifier lists 
    55   * allow variables that are not mentioned in the body of a type (but warn) 
    56   * allow predicates that do not mention quantified variables (but warn?) 
    57  
    58  
    59 === Strict Fields === 
    60  
    61 The fields in 'data' constructors may be annotated with '!', indicating 
    62 that they are strict.  Where should we place the '!' for a polymorphic field? 
    63 It appears that this is not supported in Hugs (bug? I have not looked at 
    64 the parser). In GHC, the '!' is placed before a schema and the schema has to 
    65 be in parens (i.e. syntactically, a schema is just another 'type'). 
    66  
    67 Example: 
    68 {{{ 
    69 data T = C !(forall a. a -> a) Int 
    70 }}} 
    71 PROPOSAL: GHC's choice seems reasonable. 
    72  
    73 === Labeled Fields, Infix Constructors === 
    74  
    75 Again, we treat schemes as if they belong to category 'type'. 
    76  
    77 Examples: 
    78 {{{ 
    79 data T = C { f1 :: forall a. a -> a, f2 :: Int } 
    80 data T = (forall a. a -> a) :+: (forall x. x -> x) 
    81 }}} 
    82 In the second example we need the parens to turn 'type' into 'atype'. 
    83  
    84 One issue with labelled fields is that Haskell 98 requers that if a label appears in different constructors of a datatype, then the labelled fields should have the same type.   In the presences of polymorphic components, this translates to deciding if two schemas are equal, so we need to decide how that should work.  It seems that at present, Hugs and GHC consider two schemas to be the same if they are syntactically the same (up to alpha renaming).    
    85  
    86 Examples: 
    87 {{{ 
    88 forall a. a -> a 
    89 === 
    90 forall b. b -> b 
    91 }}} 
    92 {{{ 
    93 forall a. (Eq a, Show a) => a -> a 
    94 =/= 
    95 forall a. (Show a, Eq a) => a -> a 
    96 }}} 
    97  
    98 The second example might be a bit surprising.  Other options: 
    99   * Allow syntactic permutations of the predicates (i.e., compare them as sets of predicates rather then lists of predicates) 
    100   * Use entailment: 
    101 {{{ 
    102 (forall as. ps => s) === (forall bs. qs => t) 
    103 iff 
    104 1) forall bs. exist as. (qs |- ps) /\ (s = t), and 
    105 2) forall as. exist bs. (ps |- qs) /\ (s = t) 
    106 }}} 
    107  
    108 PROPOSAL: Use syntactic equivalence modulo 
    109   * alpha renamimng 
    110   * order/repetition of predicates (i.e. compare predicates as sets) 
    111  
    112 == Constructors == 
    113  
    114 Constructor that have polymorphic components cannot appear in the 
    115 program without values for their polymorphic fields.  For example, 
    116 consider the following declaration: 
    117 {{{ 
    118 data T a  = C Int (forall b. b -> a) a 
    119 }}} 
    120 The constructor function 'C' should always be applied to at least 
    121 two arguments because the second argument is the last polymorphic component 
    122 of 'C'.  Here are some examples of how we can use 'C': 
    123 {{{ 
    124 ex1 :: a -> T a 
    125 ex1 a = C 2 (const a)      -- ok. 
    126  
    127 ex2 = C 2                  -- not ok, needs another argument. 
    128 }}} 
    129 (This issue is related to the treatment of rank-2 types and the choice here should be consistent with that extension.) 
    130  
    131 The restriction that functions with rank-2 types are applied to all their polymorphic arguments ensures that all expressions have ordinary (i.e., non rank-2) types, as in Haskell 98. 
    132  
    133 Here is an example that illustrates some of the difficulties that arise if we allow partially applied constructors: 
    134 {{{ 
    135 data T  = C1 Int (forall a. (Eq a, Show a) => a -> a) 
    136         | C2     (forall a. (Show a, Eq a) => a -> a) 
    137  
    138 h      :: a -> a -> Int 
    139 h _ _   = 1 
    140  
    141 test    = h (C1 1) C2 
    142 }}} 
    143  
    144  
    145  
    146 == Pattern matching == 
    147  
    148 We do not allow nested patterns on fields that have polymorphic types. 
    149 In other words, when we use a constructor with a polymorphic field 
    150 as a pattern, we allow only variable and wild-card patterns in the 
    151 positions corresponding to the polymorphic fields. 
    152  
    153 Example: 
    154 {{{ 
    155 newtype PolyList = C (forall a. [a]) 
    156  
    157 polyNull (C []) = True    -- disallowed, nested pattern on a poly. field 
    158 polyNull _      = False 
    159 }}} 
    160 This is the behavior of both Hugs and GHC at present.