Changes between Version 18 and Version 19 of Roles

Jun 25, 2017 5:18:18 AM (2 years ago)

Roles for type families


  • Roles

    v18 v19  
    206206this not-quite-as-safe GND could use unsafeCoerce wherever the safe
    207207one would give an error about annotated roles.
     209= Proposal: roles for type families =
     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.
     213== Examples we cannot write today ==
     215This example ([ courtesy of glguy]) will not typecheck:
     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
     223coerceOp :: Coercible a b => Op n a c -> Op n b c
     224coerceOp = coerce
     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.
     229Another example ([ courtesy of int-index]) is:
     232-- represents effect methods for some monad `m`
     233data family EffDict (eff :: k) (m :: Type -> Type)
     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 () }
     243-- composition of monad transformers
     244newtype TComp t1 t2 m a = TComp (t1 (t2 m) a)
     246coerceDict :: EffDict eff (t1 (t2 m)) -> EffDict eff (TComp t1 t2 m)
     247coerceDict = coerce
     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.)
     252Additionally, we might like to have roles for //associated// type families. For instance, consider this example ([ courtesy of dmcclean]):
     255data Variant = DQuantity | DUnit Prefixability
     256data Dimension
     258class KnownVariant (var :: Variant) where
     259  data Dimensional var :: Dimension -> * -> *
     261instance KnownVariant DQuantity where
     262  newtype Dimensional DQuantity d v = Quantity' v
     264instance KnownVariant (DUnit p) where
     265  data Dimensional (DUnit p) d v = Unit' UnitName v
     267type Quantity = Dimensional DQuantity
     268coerceQuantity :: Coercible v w => Quantity d v -> Quantity d w
     269coerceQuantity = coerce
     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.
     274== Syntax ==
     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.,
     279type role F nominal
     280type family F a
     283But this is a restriction that is easily overcome. In addition, the parser does not currently recognize role annotations for associated type families:
     286class C a where
     287  type role Assoc nominal nominal
     288  type Assoc a b
     291But this could be added without much difficulty.
     293== Role inference for type families ==
     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.
     297=== Example ===
     299Consider this type family:
     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
     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.
     310=== The type family kind ===
     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.
     314=== The type family equations ===
     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 [ 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`.
     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:
     321type family Inspect x where
     322  Inspect Bool = Int
     323  Inspect Int  = Bool
     325coerceInspect :: Coercible a b => Inspect a -> Inspect b
     326coerceInspect = coerce
     328unsafeBoolToInt :: Bool -> Int
     329unsafeBoolToInt = (coerceInspect :: Inspect Int -> Inspect Age)
     332To accomplish this, we check for any occurences of the either of the following sorts of scrutinization:
     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:
     337type family Inspect x where
     338  Inspect Int          = Bool
     339  Inspect (Either a b) = a
     340  Inspect (f a)        = a
     343   Any type variable that is scrutinized in this fashion (`x` in the above example) is marked as `nominal`.
     3452. Type patterns that are syntactically equal are all marked as nominal. For instance:
     348type family Eq w x y z where
     349  Eq a b (Either b a) c = a
     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`.
     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`.
     356== Role checking for type families ==
     358Users can also specify role annotations for type families that should be checked against the inferred roles. For instance:
     361type role G nominal nominal
     362type family G a b where
     363  G a b = Either a b
     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`.
     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?
     371type family Open a b
     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.
     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.,
     379type role Open representational representational
     380type family Open a b
     383== Type family roles and hs-boot files ==
     385Just like we default roles for open type families to `nominal`, we do the same for type families declared in `hs-boot` files.