Changes between Version 19 and Version 20 of Roles


Ignore:
Timestamp:
Jun 25, 2017 11:10:06 AM (2 years ago)
Author:
goldfire
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • Roles

    v19 v20  
    225225}}}
    226226
    227 Since the role signature for `Op` is `type role Op nominal nominal nominal`. But in an ideal world, the role signature for `Op` would be inferred as `type role Op nominal representational representational`. After all, neither `a` nor `b` is "scrutinized" in any sense, so it feels perfectly safe to coerce them freely.
     227Since the role signature for `Op` is `type role Op nominal nominal nominal`. But in an ideal world, the role signature for `Op` would be inferred as `type role Op nominal representational representational`. After all, neither `a` nor `b` is "scrutinized" in any sense, so it feels perfectly safe to coerce them freely. '''RAE:''' "feels"? Let's prove it! '''End RAE'''
    228228
    229229Another example ([https://ghc.haskell.org/trac/ghc/ticket/8177#comment:33 courtesy of int-index]) is:
     
    283283But this is a restriction that is easily overcome. In addition, the parser does not currently recognize role annotations for associated type families:
    284284
    285 {{#!hs
     285{{{#!hs
    286286class C a where
    287287  type role Assoc nominal nominal
     
    290290
    291291But this could be added without much difficulty.
     292
     293'''RAE:''' There is a difference between roles for
     294data families and data instances. And both might usefully
     295have role annotations. For example:
     296
     297{{{#!hs
     298
     299data family DF a b
     300type role DF nominal representational
     301
     302data instance DF Int b = MkDFInt b
     303 -- NB: No scrutinizing the second parameter.
     304 -- Also, b is not used in a nominal context
     305
     306data instance DF [c] b = MkDFList c b
     307type role DF [nominal] representational
     308
     309data instance DF (Maybe d) b = MkDFMaybe d b
     310type role DF (Maybe representational) representational
     311}}}
     312
     313With this, we have `Coercible (DF (Maybe Age) Int) (DF (Maybe Int) Age)` but not `Coercible (DF [Age] Int) (DF [Int] Age)`.
     314
     315I ''think'' (but have not ever tried to prove) that these instance roles would work out, with the following restrictions:
     316
     317 * If a data family parameter is not scrutinized (that is, it's just a bare variable), then the instance role must match the family role exactly.
     318
     319 * Corollary: all representational/phantom roles from the family must be repeated exactly in the instances.
     320
     321 * Other variables may be given new roles according to the usual rules, including the usage of the variable in the instance head as a usage site. (That is, if the variable is used in a nominal context in the instance head, then it must be marked nominal.)
     322
     323I'm a bit worried about problems with what happens if a type constructor that appears as part of a type pattern for an instance is actually a newtype with a role annotation -- could we be breaking soundness with this? Need to think harder.
     324
     325'''End RAE'''
    292326
    293327== Role inference for type families ==
     
    310344=== The type family kind ===
    311345
    312 First, we gather all of the free variables in the type family's kind and mark each as `nominal`. This is under the observation that only type variables can be at role `phantom` or `nominal`, never kind variables. Therefore, `k` would be marked as nominal.
     346First, we gather all of the free variables in the type family's kind and mark each as `nominal`. This is under the observation that only type variables can be at role `phantom` or `representational`, never kind variables. Therefore, `k` would be marked as nominal.
    313347
    314348=== The type family equations ===
     
    354388Returning to the earlier `F` example, we would learn that `e` and `g` should be marked nominal, as they are both scrutinized. Therefore, the final inferred roles for `k`, `e`, `f`, `g`, and `h` are `nominal`, `nominal`, `representational`, `nominal`, and `phantom`.
    355389
     390'''RAE:''' This works well for ''closed'' type families, but is ineffective with open type/data families (associated or not). I propose that open families default to nominal roles. This is quite like how open families' type variables default to kind `Type`. Edit: I see this addressed below, but the opening paragraph for this section mentions inference for open families. '''End RAE'''
     391
    356392== Role checking for type families ==
    357393