Changes between Version 13 and Version 14 of InjectiveTypeFamilies


Ignore:
Timestamp:
Oct 8, 2014 7:58:49 AM (5 years ago)
Author:
jstolarek
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • InjectiveTypeFamilies

    v13 v14  
    7474== Proposed syntax
    7575
    76 Below is a list of various syntax proposed so far for this new feature. Two
    77 important things to consider when deciding on a concrete syntax are:
     76Two important things to consider when deciding on a concrete syntax are:
    7877
    7978  * '''Backwards compatibility''': at the moment no decision has been made on
     
    8887    to add B and C in the future without breaking A.
    8988
    90 === Proposal 1
    91 
    92 Use syntax similar to functional dependencies. The injectivity declaration
    93 begins with `|` following type family declaration head. `|` is followed by a
    94 list of comma-separated injectivity conditions. Each injectivity condition has
    95 the form:
    96 
    97 {{{#!hs
    98 result A -> B
    99 }}}
    100 
    101 where `A` is a possibly-empty list of type variables declared in type family
    102 head and `B` is non-empty list of said type variables. Things on the left and
    103 right of `->` are called LHS and RHS of an injectivity condition,
    104 respectively. `result` becomes a restricted word that cannot be used as a type
    105 variable's identifier in a type family head.  I think this is identical to how
    106 the `role` word is treated. Examples (taken from the previous section):
    107 
    108 {{{#!hs
    109 type family Id a     | result -> a where
    110 type family F a b c  | result -> a b c
    111 type family G a b c  | result -> a b where
    112 type family Plus a b | result a -> b, result b -> a where
    113 type family H a b c  | result a -> b c, result b -> a c
    114 }}}
     89We decided to use syntax similar to functional dependencies.  The injectivity
     90declaration begins with `|` following type family declaration head.  `|` is
     91followed by a list of comma-separated injectivity conditions. Each injectivity
     92condition has the form:
     93
     94{{{#!hs
     95A -> B
     96}}}
     97
     98where `A` and `B` are non-empty lists of type variables declared in type family
     99head. Things on the left and right of `->` are called LHS and RHS of an
     100injectivity condition, respectively. The user must be able to name the result of
     101a type family. To achieve that we extend syntax of type family head by allowing
     102to write `= tyvar` or `= (tyvar :: kind)` annotations in addition to already
     103allowed `:: kind` annotation. In other words all these declaration are
     104well-formed:
     105
     106{{{#!hs
     107type family Plus (a :: Nat) (b :: Nat) where ...
     108type family Plus (a :: Nat) (b :: Nat) :: Nat where ...
     109type family Plus (a :: Nat) (b :: Nat) = c where ...
     110type family Plus (a :: Nat) (b :: Nat) = (c :: Nat) where ...
     111}}}
     112
     113but the third or fourth form is required if the user wants to introduce
     114injectivity declaration. Here are examples of injectivity declarations using
     115proposed syntax:
     116
     117{{{#!hs
     118type family Id a = result | result -> a where
     119type family F a b c = d | d -> a b c
     120type family G a b c = foo | foo -> a b where
     121type family Plus a b = (sum :: Nat) | sum a -> b, sum b -> a where
     122type family H a b c = xyz | xyz a -> b c, xyz b -> a c
     123}}}
     124
     125Note that above examples demonstrate all three types of injectivivity but for
     126now we only plan to implement injectivity A.
    115127
    116128Pros:
    117129
    118   * has natural reading: `result a -> b` reads as "knowing the result and the
    119     type variable a determines b".
     130  * natural reading: `res a -> b` reads as "knowing res and a determines b".
    120131
    121132  * extensible for the future
    122133
     134  * backwards compatible
     135
    123136Cons:
    124137
    125   * steals `result` identifier in the type family head. This means it would be
    126     illegal to have a type variable named `result` in a type family.
    127 
    128   * the above makes this proposal backwards incompatible with `TypeFamilies`
    129     extension.
    130 
    131 Further proposals are based on this one in an attempt to solve the problem of
    132 stealing syntax and backwards incompatibility.
    133 
    134 
    135 === Proposal 2
    136 
    137 Use `Result` instead of `result`:
    138 
    139 {{{#!hs
    140 type family Id a     | Result -> a where
    141 type family F a b c  | Result -> a b c
    142 type family G a b c  | Result -> a b where
    143 type family Plus a b | Result a -> b, Result b -> a where
    144 type family H a b c  | Result a -> b c, Result b -> a c
    145 }}}
    146 
    147 Pros:
    148 
    149   * has natural reading
    150 
    151   * extensible for the future
    152 
    153   * allows to have type variables named `result` (does not steal syntax)
    154 
    155 Cons:
    156 
    157   * all other keywords in Haskell are lower case. This would be the first one
    158     that is capitalized.
    159 
    160   * confusion could arise if we have a type `Result` and use it in the type
    161     family head.
    162 
    163 Unknowns (for me):
    164 
    165   * not sure if it would be possible to avoid name clash between `Result` and
    166     type of the same name. If not then this proposal would also be backwards
    167     incompatible with `TypeFamilies`.
    168 
    169 
    170 === Proposal 3
    171 
    172 Use `type` instead of `result`:
    173 
    174 {{{#!hs
    175 type family Id a     | type -> a where
    176 type family F a b c  | type -> a b c
    177 type family G a b c  | type -> a b where
    178 type family Plus a b | type a -> b, type b -> a where
    179 type family H a b c  | type a -> b c, type b -> a c
    180 }}}
    181 
    182 Pros:
    183 
    184   * extensible for the future
    185 
    186   * no syntax stealing
    187 
    188 Cons:
    189 
    190   * no natural reading
    191 
    192   * usage of `type` here might seem unintuitive
    193 
    194 
    195 === Proposal 4
    196 
    197 Use name of the type family instead of `result`:
    198 
    199 {{{#!hs
    200 type family Id a     | Id -> a where
    201 type family F a b c  | F -> a b c
    202 type family G a b c  | G -> a b where
    203 type family Plus a b | Plus a -> b, Plus b -> a where
    204 type family H a b c  | H a -> b c, H b -> a c
    205 }}}
    206 
    207 Pros:
    208 
    209   * extensible for the future
    210 
    211   * no syntax stealing
    212 
    213 Cons:
    214 
    215   * writing something like `Plus a` might be confusing. It looks as if `Plus`
    216     could be partially applied.
    217 
    218 === Proposal 5
    219 
    220 A major drawback of all proposals 1-4, 6-7 is that if we only implement A injectivity then writing things like `result -> a b c d` is a lot of boilerplate (since there is only one possible injectivity condition anyway). We could avoid that by introducing `injective` keyword:
    221 
    222 {{{#!hs
    223 injective type family Id a where
    224 injective type family F a b c
    225 injective type family G a b c  where
    226 injective type family Plus a b where
    227 injective type family H a b c
    228 }}}
    229 
    230 Pros:
    231 
    232   * no boilerplate for declaring A injectivity
    233 
    234   * probably backwards compatible, since there is only one place where the `injective` keyword may go.
    235 
    236   * could be extended in the future be allowing any of the proposals 1-4 to be used alternatively
    237 
    238 Cons:
    239 
    240   * steals "injective" identifier in type family head (I think)
    241 
    242   * not directly extensible. Introducing syntax from proposals 1-4 sometime in the future will end up with redundancy
    243 
    244 === Proposal 6
    245 
    246 Don't write the `result`:
    247 
    248 {{{#!hs
    249 type family Id a     | -> a where
    250 type family F a b c  | -> a b c
    251 type family G a b c  | -> a b where
    252 type family Plus a b | a -> b, b -> a where
    253 type family H a b c  | a -> b c, b -> a c
    254 }}}
    255 
    256 Pros:
    257 
    258   * extensible for the future
    259 
    260   * backwards compatible
    261 
    262 Cons:
    263 
    264   * might be a bit confusing?
    265 
    266 === Proposal 7
    267 
    268 Use type variable that names the RHS instead of `result`:
    269 
    270 {{{#!hs
    271 type family Id a :: result | result -> a where
    272 type family F a b c :: d | d -> a b c
    273 type family G a b c :: foo | foo-> a b where
    274 type family Plus a b :: sum | sum a -> b, sum b -> a where
    275 type family H a b c :: xyz | xyz a -> b c, xyz b -> a c
    276 }}}
    277 
    278 Pros:
    279 
    280   * extensible for the future
    281 
    282   * backwards compatible
    283 
    284   * we already allow naming the RHS in this way
    285 
    286 Cons:
    287 
    288   * ?
     138  * since we only plan to implement injectivity of form A we require that there
     139    is only one injectivity condition, its LHS contains only a type variable
     140    naming the result and its RHS contains all type variables naming the
     141    arguments to a type family. This might be a bit annoying.
     142
    289143
    290144== Real-life use cases