Changes between Version 10 and Version 11 of Ticket #57


Ignore:
Timestamp:
Apr 4, 2007 10:34:29 PM (8 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.