diff options
Diffstat (limited to 'docs/users_guide/exts/roles.rst')
| -rw-r--r-- | docs/users_guide/exts/roles.rst | 228 |
1 files changed, 228 insertions, 0 deletions
diff --git a/docs/users_guide/exts/roles.rst b/docs/users_guide/exts/roles.rst new file mode 100644 index 0000000000..a92a78787d --- /dev/null +++ b/docs/users_guide/exts/roles.rst @@ -0,0 +1,228 @@ +.. _roles: + +Roles +===== + +.. index:: + single: roles + +Using :extension:`GeneralizedNewtypeDeriving` +(:ref:`newtype-deriving`), a programmer can take existing +instances of classes and "lift" these into instances of that class for a +newtype. However, this is not always safe. For example, consider the +following: + +:: + + newtype Age = MkAge { unAge :: Int } + + type family Inspect x + type instance Inspect Age = Int + type instance Inspect Int = Bool + + class BadIdea a where + bad :: a -> Inspect a + + instance BadIdea Int where + bad = (> 0) + + deriving instance BadIdea Age -- not allowed! + +If the derived instance were allowed, what would the type of its method +``bad`` be? It would seem to be ``Age -> Inspect Age``, which is +equivalent to ``Age -> Int``, according to the type family ``Inspect``. +Yet, if we simply adapt the implementation from the instance for +``Int``, the implementation for ``bad`` produces a ``Bool``, and we have +trouble. + +The way to identify such situations is to have *roles* assigned to type +variables of datatypes, classes, and type synonyms. + +Roles as implemented in GHC are a from a simplified version of the work +described in `Generative type abstraction and type-level +computation <http://www.seas.upenn.edu/~sweirich/papers/popl163af-weirich.pdf>`__, +published at POPL 2011. + +.. _nominal-representational-and-phantom: + +Nominal, Representational, and Phantom +-------------------------------------- + +.. index:: + single: representational; role + single: nominal; role + single: phantom; role + +The goal of the roles system is to track when two types have the same +underlying representation. In the example above, ``Age`` and ``Int`` +have the same representation. But, the corresponding instances of +``BadIdea`` would *not* have the same representation, because the types +of the implementations of ``bad`` would be different. + +Suppose we have two uses of a type constructor, each applied to the same +parameters except for one difference. (For example, ``T Age Bool c`` and +``T Int Bool c`` for some type ``T``.) The role of a type parameter says +what we need to know about the two differing type arguments in order to +know that the two outer types have the same representation (in the +example, what must be true about ``Age`` and ``Int`` in order to show +that ``T Age Bool c`` has the same representation as ``T Int Bool c``). + +GHC supports three different roles for type parameters: nominal, +representational, and phantom. If a type parameter has a nominal role, +then the two types that differ must not actually differ at all: they +must be identical (after type family reduction). If a type parameter has +a representational role, then the two types must have the same +representation. (If ``T``\'s first parameter's role is representational, +then ``T Age Bool c`` and ``T Int Bool c`` would have the same +representation, because ``Age`` and ``Int`` have the same +representation.) If a type parameter has a phantom role, then we need no +further information. + +Here are some examples: :: + + data Simple a = MkSimple a -- a has role representational + + type family F + type instance F Int = Bool + type instance F Age = Char + + data Complex a = MkComplex (F a) -- a has role nominal + + data Phant a = MkPhant Bool -- a has role phantom + +The type ``Simple`` has its parameter at role representational, which is +generally the most common case. ``Simple Age`` would have the same +representation as ``Simple Int``. The type ``Complex``, on the other +hand, has its parameter at role nominal, because ``Complex Age`` and +``Complex Int`` are *not* the same. Lastly, ``Phant Age`` and +``Phant Bool`` have the same representation, even though ``Age`` and +``Bool`` are unrelated. + +.. _role-inference: + +Role inference +-------------- + +What role should a given type parameter should have? GHC performs role +inference to determine the correct role for every parameter. It starts +with a few base facts: ``(->)`` has two representational parameters; +``(~)`` has two nominal parameters; all type families' parameters are +nominal; and all GADT-like parameters are nominal. Then, these facts are +propagated to all places where these types are used. The default role +for datatypes and synonyms is phantom; the default role for classes is +nominal. Thus, for datatypes and synonyms, any parameters unused in the +right-hand side (or used only in other types in phantom positions) will +be phantom. Whenever a parameter is used in a representational position +(that is, used as a type argument to a constructor whose corresponding +variable is at role representational), we raise its role from phantom to +representational. Similarly, when a parameter is used in a nominal +position, its role is upgraded to nominal. We never downgrade a role +from nominal to phantom or representational, or from representational to +phantom. In this way, we infer the most-general role for each parameter. + +Classes have their roles default to nominal to promote coherence of +class instances. If a ``C Int`` were stored in a datatype, it would be +quite bad if that were somehow changed into a ``C Age`` somewhere, +especially if another ``C Age`` had been declared! + +There is one particularly tricky case that should be explained: :: + + data Tricky a b = MkTricky (a b) + +What should ``Tricky``'s roles be? At first blush, it would seem that +both ``a`` and ``b`` should be at role representational, since both are +used in the right-hand side and neither is involved in a type family. +However, this would be wrong, as the following example shows: :: + + data Nom a = MkNom (F a) -- type family F from example above + +Is ``Tricky Nom Age`` representationally equal to ``Tricky Nom Int``? +No! The former stores a ``Char`` and the latter stores a ``Bool``. The +solution to this is to require all parameters to type variables to have +role nominal. Thus, GHC would infer role representational for ``a`` but +role nominal for ``b``. + +.. _role-annotations: + +Role annotations +---------------- + +.. extension:: RoleAnnotations + :shortdesc: Enable role annotations. + + :since: 7.8.1 + + Allow role annotation syntax. + +Sometimes the programmer wants to constrain the inference process. For +example, the base library contains the following definition: :: + + data Ptr a = Ptr Addr# + +The idea is that ``a`` should really be a representational parameter, +but role inference assigns it to phantom. This makes some level of +sense: a pointer to an ``Int`` really is representationally the same as +a pointer to a ``Bool``. But, that's not at all how we want to use +``Ptr``\ s! So, we want to be able to say :: + + type role Ptr representational + data Ptr a = Ptr Addr# + +The ``type role`` (enabled with :extension:`RoleAnnotations`) declaration +forces the parameter ``a`` to be at role representational, not role +phantom. GHC then checks the user-supplied roles to make sure they don't +break any promises. It would be bad, for example, if the user could make +``BadIdea``\'s role be representational. + +As another example, we can consider a type ``Set a`` that represents a +set of data, ordered according to ``a``\'s ``Ord`` instance. While it +would generally be type-safe to consider ``a`` to be at role +representational, it is possible that a ``newtype`` and its base type +have *different* orderings encoded in their respective ``Ord`` +instances. This would lead to misbehavior at runtime. So, the author of +the ``Set`` datatype would like its parameter to be at role nominal. +This would be done with a declaration :: + + type role Set nominal + +Role annotations can also be used should a programmer wish to write a +class with a representational (or phantom) role. However, as a class +with non-nominal roles can quickly lead to class instance incoherence, +it is necessary to also specify :extension:`IncoherentInstances` to allow +non-nominal roles for classes. + +The other place where role annotations may be necessary are in +``hs-boot`` files (:ref:`mutual-recursion`), where the right-hand sides +of definitions can be omitted. As usual, the types/classes declared in +an ``hs-boot`` file must match up with the definitions in the ``hs`` +file, including down to the roles. The default role for datatypes is +representational in ``hs-boot`` files, corresponding to the common use +case. + +Role annotations are allowed on data, newtype, and class declarations. A +role annotation declaration starts with ``type role`` and is followed by +one role listing for each parameter of the type. (This parameter count +includes parameters implicitly specified by a kind signature in a +GADT-style data or newtype declaration.) Each role listing is a role +(``nominal``, ``representational``, or ``phantom``) or a ``_``. Using a +``_`` says that GHC should infer that role. The role annotation may go +anywhere in the same module as the datatype or class definition (much +like a value-level type signature). Here are some examples: :: + + type role T1 _ phantom + data T1 a b = MkT1 a -- b is not used; annotation is fine but unnecessary + + type role T2 _ phantom + data T2 a b = MkT2 b -- ERROR: b is used and cannot be phantom + + type role T3 _ nominal + data T3 a b = MkT3 a -- OK: nominal is higher than necessary, but safe + + type role T4 nominal + data T4 a = MkT4 (a Int) -- OK, but nominal is higher than necessary + + type role C representational _ -- OK, with -XIncoherentInstances + class C a b where ... -- OK, b will get a nominal role + + type role X nominal + type X a = ... -- ERROR: role annotations not allowed for type synonyms |