Changes between Version 1 and Version 2 of RolesImplementation


Ignore:
Timestamp:
Jul 25, 2013 1:27:40 PM (9 months ago)
Author:
goldfire
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • RolesImplementation

    v1 v2  
    1 For Richard E TODO: Write this page. 
    2 Deadline: Aug 2, 2013. 
     1= Roles Implementation = 
     2 
     3This page describes how roles are implemented in GHC. If you're looking for how 
     4to use roles in a Haskell program, see [wiki:Roles]. 
     5 
     6== The `Role` datatype == 
     7 
     8The `Role` datatype, defined in `CoAxiom` to avoid mentioning it in an hs-boot 
     9file, is defined thusly: 
     10 
     11{{{ 
     12data Role = Nominal | Representational | Phantom 
     13  deriving (Eq, Data.Data, Data.Typeable) 
     14}}} 
     15 
     16Two types are nominally equal when they have the same name. This is the usual 
     17equality in Haskell or Core. Two types are representationally equal when they 
     18have the same representation. (If a type is higher-kinded, all nominally equal 
     19instantiations lead to representationally equal types.) Any two types are 
     20"phantomly" equal. 
     21 
     22== Roles on `Coercion`s == 
     23 
     24Every coercion proves an equality at a certain role. There are subtle rules 
     25governing what compositions are allowed. See 
     26[[http://github.com/ghc/ghc/blob/master/docs/core-spec/core-spec.pdf?raw=true|the core spec]] for the details, or look at `coercionRole`. To facilitate this, 
     27a few of the `Coercion` constructors needed to be changed: 
     28 
     29 * `Refl` now takes a role and a type, proving reflexive equality at the given role. 
     30 * `TyConAppCo` also takes a role. The choice of this role affects which roles the 
     31   arguments must be at. If the role is nominal, all arguments must be nominal. 
     32   If the role is phantom, all arguments must be phantom. But, if the role is 
     33   representational, the argument roles must correspond to `tyConRoles` called 
     34   on the tycon in the `TyConAppCo`. The idea is that different tycons have 
     35   different requirements in order to prove representational equality. See the 
     36   section below discussing roles with tycons. Note that, now, the interpretation 
     37   of a `TyConAppCo` may differ from that of nested `AppCo`s. 
     38 * `CoVarCo`s extract their role from their type. 
     39 * `UnivCo` is a new "universal" coercion. It takes a role and two types and witnesses 
     40   equality between those types at that role. It replaces the old `UnsafeCo`. 
     41   `UnivCo` at role P is needed in `TyConAppCo`s at role P. 
     42 * The role produced by `NthCo` is essentially the inverse of the `TyConAppCo` story. 
     43   If `NthCo`'s parameter is N or P, the result has the same role. If it's R, though, 
     44   the result's role is determined by `tyConRoles` once again. 
     45 * `SubCo` implements sub-roling: its argument is N and it produces R. 
     46 
     47Because coercions can be produced at any of the three roles, most functions that 
     48produce them now take a `Role` parameter, indicating what role to produce. These, 
     49in turn, make use of `maybeSubCo2` and `maybeSubCo`, which convert among the roles; 
     50they are documented in the source. 
     51 
     52The functions `mkTyConAppCo` (and, in turn `mkFunCo`) now have a bit of a delicate 
     53requirement on their arguments: the argument types must "match" the desired role. 
     54Thus, if the desired role is R, the arguments must have the roles indicated by 
     55`tyConRoles`. In practice, it is not hard to ensure this precondition, but you 
     56do have to be aware of it. 
     57 
     58== Roles on `TcCoercion`s == 
     59 
     60The type checker operates solely on `TcCoercion`s. What roles do these have? Because 
     61the type checker thinks only about nominal equality, it would make sense for all 
     62`TcCoercion`s to have role N. But, sometimes the type checker needs to pass around 
     63a coercion produced by a newtype (for example, in implicit-parameter handling). 
     64So, they need to handle R coercions as well. But, we never lint a `TcCoercion`, so 
     65we don't quite need to be as careful with them. 
     66 
     67The solution is that, when desugaring to `Coercion`s, we pass in a `Role` 
     68parameter, indicating how we should interpret the `TcCoercion`. (Casts always 
     69use R equality.) Because we hopefully never ask for nominal equality from a 
     70newtype axiom, this works in practice. If a problem arises, it will most likely 
     71take the form of a `maybeSubCo2` panic. 
     72 
     73== Roles with `TyCon`s == 
     74 
     75Every `TyCon`'s parameters are now each assigned a role. The interpretation is 
     76this: if a parameter a of tycon T has role r, then a coercion at role r can be 
     77lifted into a representational coercion of T a. Thus, N is the most 
     78restrictive, and P is the most permissive. These roles are user-visible, so 
     79they are described on the [wiki:Roles] page. 
     80 
     81Kind variables are all assigned role N. We must be careful when comparing a 
     82tycon's roles against the role annotations, because role annotations are only 
     83on ''type'' variables, never ''kind'' variables. So, we often have to drop 
     84the kind-variable roles when doing the comparison. 
     85 
     86== `eqPrimTyCon` vs `eqReprPrimTyCon` == 
     87 
     88The type of a nominal coercion is headed by `eqPrimTyCon`, spelled `~#`. In 
     89order to support NewtypeWrappers, we must also have a way of storing 
     90representational coercions. Their types are headed by `eqReprPrimTyCon`, spelled 
     91`~R#`.