Changes between Version 18 and Version 19 of Roles


Ignore:
Timestamp:
Jun 25, 2017 5:18:18 AM (2 years ago)
Author:
RyanGlScott
Comment:

Roles for type families

Legend:

Unmodified
Added
Removed
Modified
  • Roles

    v18 v19  
    206206this not-quite-as-safe GND could use unsafeCoerce wherever the safe
    207207one would give an error about annotated roles.
     208
     209= Proposal: roles for type families =
     210
     211Currently, the type constructors for all type families and data families all conservatively assign role `nominal` to all their parameters. This is a safe choice, but a restrictive one, as it rules out some useful, coercion-safe programs. In this section, I propose a way to allow type families to have parameters with phantom and representational roles.
     212
     213== Examples we cannot write today ==
     214
     215This example ([https://ghc.haskell.org/trac/ghc/ticket/8177#comment:32 courtesy of glguy]) will not typecheck:
     216
     217{{{#!hs
     218-- | Family of N-ary operator types.
     219type family Op n a b where
     220  Op 'Z     a b = b
     221  Op ('S n) a b = a -> Op n a b
     222
     223coerceOp :: Coercible a b => Op n a c -> Op n b c
     224coerceOp = coerce
     225}}}
     226
     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.
     228
     229Another example ([https://ghc.haskell.org/trac/ghc/ticket/8177#comment:33 courtesy of int-index]) is:
     230
     231{{{#!hs
     232-- represents effect methods for some monad `m`
     233data family EffDict (eff :: k) (m :: Type -> Type)
     234
     235-- Note this matches on `eff`, not `m`
     236data StateEff s
     237data instance EffDict (StateEff s) m =
     238  StateDict
     239    { _state :: forall a . (s -> (a,s)) -> m a,
     240      _get :: m s,
     241      _put :: s -> m () }
     242
     243-- composition of monad transformers
     244newtype TComp t1 t2 m a = TComp (t1 (t2 m) a)
     245
     246coerceDict :: EffDict eff (t1 (t2 m)) -> EffDict eff (TComp t1 t2 m)
     247coerceDict = coerce
     248}}}
     249
     250Again, `coerceDict` will not typecheck due to the role of `m` in `EffDict` being `nominal`. But there's no good reason why this //must// be the case—we ought to be able to tell GHC to allow `m` to have `representational role`. (Of course, this would prevent any `EffDict` instance from using `m` at a `nominal` role, but them's the breaks.)
     251
     252Additionally, we might like to have roles for //associated// type families. For instance, consider this example ([https://ghc.haskell.org/trac/ghc/ticket/8177#comment:20 courtesy of dmcclean]):
     253
     254{{{#!hs
     255data Variant = DQuantity | DUnit Prefixability
     256data Dimension
     257
     258class KnownVariant (var :: Variant) where
     259  data Dimensional var :: Dimension -> * -> *
     260
     261instance KnownVariant DQuantity where
     262  newtype Dimensional DQuantity d v = Quantity' v
     263
     264instance KnownVariant (DUnit p) where
     265  data Dimensional (DUnit p) d v = Unit' UnitName v
     266
     267type Quantity = Dimensional DQuantity
     268coerceQuantity :: Coercible v w => Quantity d v -> Quantity d w
     269coerceQuantity = coerce
     270}}}
     271
     272Once again, `coerceQuantity` is ill typed, simply because of the conservative `nominal` role that the last type parameter of `Dimensional` has. Associated type families are an interesting case, since they can have extra type parameters (and thus extra roles) that the parent class does not have.
     273
     274== Syntax ==
     275
     276Implementing roles for type families would not require too many changes to the syntax of the language, as most of the required pieces are already there. The biggest current restriction is the fact that one cannot declare role annotations for type families, e.g.,
     277
     278{{{#!hs
     279type role F nominal
     280type family F a
     281}}}
     282
     283But this is a restriction that is easily overcome. In addition, the parser does not currently recognize role annotations for associated type families:
     284
     285{{#!hs
     286class C a where
     287  type role Assoc nominal nominal
     288  type Assoc a b
     289}}}
     290
     291But this could be added without much difficulty.
     292
     293== Role inference for type families ==
     294
     295Regardless of whether we're dealing with a closed, open, or associated type family, GHC will need to infer the most permissive roles possible for every type family, and possibly check these roles against a user-provided role signature. This section describes how role inference will operate.
     296
     297=== Example ===
     298
     299Consider this type family:
     300
     301{{{#!hs
     302type family F (e :: *) (f :: *) (g :: *) (h :: *) :: k where
     303  F Int       b c d = c
     304  F (Maybe a) b a d = Maybe b
     305  F a         b c d = a
     306}}}
     307
     308There are five type parameters for `F`: `k`, `e`, `f`, `g`, and `h`. What should be the roles for each one? We will start off by assuming each parameter has role `phantom`, and then walk the structure of the type family, progressively marking parameters with more restrictive roles.
     309
     310=== The type family kind ===
     311
     312First, 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.
     313
     314=== The type family equations ===
     315
     316Next, we descend into each defining equation of the type family and inspect the left-hand and right-hand sides. The right-hand sides are analyzed just like the fields of a data constructor; see the [https://ghc.haskell.org/trac/ghc/wiki/Roles#Roleinference Role inference] section above for more details. From the right-hand sides, we learn that the roles of `e`, `f`, and `g` should be (at least) `representational`.
     317
     318The more interesting analysis comes when inspecting the left-hand sides. We want to mark any type variable that is //scrutinized// as `nominal`. By "scrutinized", we mean a variable that is being used in a non-parametric fashion. For instance, we want to rule out scenarios like this one:
     319
     320{{{#!hs
     321type family Inspect x where
     322  Inspect Bool = Int
     323  Inspect Int  = Bool
     324
     325coerceInspect :: Coercible a b => Inspect a -> Inspect b
     326coerceInspect = coerce
     327
     328unsafeBoolToInt :: Bool -> Int
     329unsafeBoolToInt = (coerceInspect :: Inspect Int -> Inspect Age)
     330}}}
     331
     332To accomplish this, we check for any occurences of the either of the following sorts of scrutinization:
     333
     3341. A type pattern that is not a single type variable. For instance, all of these equations provde examples of type patterns which do scrutinize a particular type variable:
     335
     336{{{#!hs
     337type family Inspect x where
     338  Inspect Int          = Bool
     339  Inspect (Either a b) = a
     340  Inspect (f a)        = a
     341}}}
     342
     343   Any type variable that is scrutinized in this fashion (`x` in the above example) is marked as `nominal`.
     344
     3452. Type patterns that are syntactically equal are all marked as nominal. For instance:
     346
     347{{{#!hs
     348type family Eq w x y z where
     349  Eq a b (Either b a) c = a
     350}}}
     351
     352   Here, we have two variable names that are used in multiple places: `a` and `b`. As a result, the type variables which they inhabit (`w`, `x`, and `y`) are all marked as `nominal`.
     353
     354Returning 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`.
     355
     356== Role checking for type families ==
     357
     358Users can also specify role annotations for type families that should be checked against the inferred roles. For instance:
     359
     360{{{#!hs
     361type role G nominal nominal
     362type family G a b where
     363  G a b = Either a b
     364}}}
     365
     366If the user hadn't written the role annotation for `G`, its role signature would have been inferred to be `type role G representational representational`. However, role checking overrides the inferred roles and assigns the more conservative roles of `type role G nominal nominal`.
     367
     368Note that while writing role annotations for //closed// type families is purely optional, it is somewhat more important for open type families. For instance, what should be the roles for this type family?
     369
     370{{{#!hs
     371type family Open a b
     372}}}
     373
     374Here, we have a choice to make. We could decide to make the roles for open type families default to, say, `representational`. While this would give us the freedom to `coerce` values of type `Open a b` more freely, it simultaneously restricts the instances we can give for `Open`, since every type instance must be checked to ensure that neither `a` nor `b` is used at a `nominal` role.
     375
     376For the sake of backwards compatibility and the principle of least surprise, roles for open type families default to `nominal`. This allows more instances to be written, but makes it harder to `coerce` them. If a user wishes to `coerce` open type families, the onus is on her to write a role annotation, e.g.,
     377
     378{{{#!hs
     379type role Open representational representational
     380type family Open a b
     381}}}
     382
     383== Type family roles and hs-boot files ==
     384
     385Just like we default roles for open type families to `nominal`, we do the same for type families declared in `hs-boot` files.