Roles: a new feature of GHC

Last week, I pushed an implementation of roles to GHC HEAD. This post explains what roles are, why they exist, and why you should care. Roles will be a part of GHC 7.8.

An old problem

Roles fix a problem in GHC’s type system that has existed for years.

The problem is the combination of GeneralizedNewtypeDeriving (henceforth called GND) and type families. An example is always best:

> {-# LANGUAGE GeneralizedNewtypeDeriving, TypeFamilies, StandaloneDeriving,
>              MultiParamTypeClasses, GADTs #-}
> 
> module Roles where
> 
> class Incrementable a where
>   incr :: a -> a
> 
> instance Incrementable Int where
>   incr x = x + 1
> 
> newtype Age = MkAge Int
>   deriving Incrementable

The idea is that, because the declaration for Age says that any Age is really just an Int in disguise, we can just re-use the instance for Incrementable Int and make it into an instance for Incrementable Age. Internally, Age has the exact same representation as Int, so GHC can really just reuse the methods that were defined for Int.

So far, so good. This makes good sense, allows for less boilerplate code, and is efficient at runtime. Yet, a problem lurks if we start using some type families:

> type family IsItAgeOrInt a
> type instance IsItAgeOrInt Int = Bool
> type instance IsItAgeOrInt Age = Char
> 
> class BadIdea a where
>   frob :: a -> IsItAgeOrInt a
> 
> instance BadIdea Int where
>   frob x = (x > 0)
> 
> deriving instance BadIdea Age

Calling frob on an Int produces nothing strange:

ghci> frob 5

  True

ghci> frob 0

  False

ghci> frob (-3)

  False

But, what happens if we call frob on an Age? According to frob’s type, calling frob on an Age should produce a IsItAgeOrInt Age – that is, a Char. But, we have reused the definition of frob for Int in the instance for Age! The result: general unhappiness:

ghci> frob (MkAge 5)
  '\-1152921504589753323'

ghci> frob (MkAge 0)
  '\4375976000'

ghci> frob (MkAge (-3))
  '\4375976000'

We’ve broken the type system.

This problem is fairly well-known. The GHC Trac has 3 bugs from it (#1496, #4846, and #7148), there was a POPL paper about it, and at least one blog post. The bug – which rightly is a flaw of the theory, not the implementation – is one of the reasons that modules with GND enabled are not considered part of the Safe Haskell subset. (The other reason is that GND can be used to break module abstraction, a subject which is not considered further here. See ticket #5498.)

The solution comes from that POPL paper: assign so-called roles to type variables to constrain how those type variables are used.

Roles

Why precisely is it a bad idea to say deriving instance BadIdea Age? Because a method in that class uses a type family in its type, and type families can tell the difference between Int and Age. The GND mechanism, though, pretends that Int and Age are the same. Thus, the two bits induce GHC to experience some cognitive dissonance, and we all suffer.

Roles label the type variables of datatypes, classes, and vanilla type synonyms indicating whether or not these all uses of these variables respect the equality between a newtype and its representation. If all uses of a variable do respect newtype-induced equalities, we say that the variable’s role is R (for “representational”). If it might be possible for a use of the variable to spot the difference between Age and Int, we say that the variable’s role is N (for “nominal”). There is a third role, P for “phantom”, which I get to later.

In our example, the parameter to Incrementable would have role R, while BadIdea would get role N. Because of these role assignments, GHC HEAD will refuse to compile the code above. It issues this error:

Can't make a derived instance of ‛BadIdea Age’
  (even with cunning newtype deriving):
  it is not type-safe to use GeneralizedNewtypeDeriving on this class;
  the last parameter of ‛BadIdea’ is at role N
In the stand-alone deriving instance for ‛BadIdea Age’

Role inference

How do we know what role to use for what parameter? We use role inference, of course! Role inference is actually quite straightforward. GHC will look at all uses of a type variable in a datatype, class, or vanilla type synonym definition and see if any of those uses are at role N. If any uses are at role N, then the variable itself must be at role N. Otherwise, (if the variable is used at all) it gets role R. The base cases are type families, (~), and certain type applications. All arguments to type families naturally get role N, as do the two arguments to the type equality operator (~). (This is because (~) will not say that Age and Int are equal.) Because GADTs are internally represented using (~), any GADT-like parameter will also be at role N.

Above, I said that certain type applications cause a role to be forced to N. This is a little subtler than the other cases, and needs an example:

> class Twiddle a b where
>   meth :: a Int -> a b
> 
> instance Twiddle [] Int where
>   meth = id
> 
> data GADT a where
>   GInt :: Int -> GADT Int
> deriving instance Show (GADT a)
> 
> instance Twiddle GADT Int where
>   meth = id
> 
> deriving instance Twiddle GADT Age
> 
> weird :: GADT Age
> weird = meth (GInt 5)

ghci> weird
  GInt 5

ghci> :t weird
  weird :: GADT Age

What’s going on here? As usual, the GND mechanism just appropriates the definition for meth wholesale for the instance for Age. That method is just the identity function. But, in the Age instance for Twiddle, the meth method has type GADT Int -> GADT Age – clearly not an identity function. Yet, it still works just fine, creating the ill-typed weird. A little more pushing here can create unsafeCoerce and segfaults.

But we already knew that GADTs behaved strangely with respect to GND. The difference in this case is that the derived class, Twiddle, does not mention any GADTs. The solution is that, whenever a type variable is used as the argument to another type variable, such as b in the definition of Twiddle, that variable gets role N. The variable a has nothing unusual about it, so it gets role R.

Phantom roles

There is ongoing work (not mine) on implementing newtype wrappers, as described here. Newtype wrappers will allow you to write code that “lifts” a newtype equality (such as the one between Age and Int) into other types (such as equating [Age] with [Int]). These lifted equalities would have no runtime cost. This is quite different than the situation today: although Age and Int can be converted for free, converting [Age] to [Int] requires iterating down the list.

With that application in mind, consider this type:

> data Phantom a = MkPhantom Int

Should we be able to convert [Phantom Bool] to [Phantom Char]? Sure we should. Labeling a’s role as P allows for this. The technical details of how P works internally are beyond the scope of this post (but you could see here for starters), but we are guaranteed that any variable at role P is never actually used in the representation of a datatype.

Role annotations

Sometimes, an implementation of an idea doesn’t quite match the abstraction. For example, the definition of Ptr, GHC’s type for pointers that might be used with foreign functions, is this:

data Ptr a = Ptr Addr#

If left to its own devices, GHC would infer role P for the type parameter a, because a is not used in the definition of Ptr. Yet, that goes against what we have in mind – we don’t really want to convert Ptr Ints to Ptr (Bool -> Bool)s willy-nilly. So, we use a role annotation (enabled with -XRoleAnnotations) which allows the programmer to override GHC’s inference, thus:

data Ptr a@R = Ptr Addr#

This role annotation (the @R) forces a’s role to be R, as desired. Note that you can’t force an unsafe role, such as requiring BadIdea’s parameter to be at role R. Role annotations only allow for stricter roling.

How does all this affect you?

Hopefully, roles won’t affect your code too much. But, it is possible that some code that has previously worked now will not. Although code breakage is rightly seen as a terrible thing, it’s actually intentional here: much of the broken code probably has a type error lurking somewhere. In my experience, there are two problems that may arise:

  • Uses of GND that worked previously and you know are safe now fail. First off, are you sure that it’s safe? Sometimes, the answer is a resounding “yes!”, but GHC still won’t let you use GND. You will have to write an instance yourself, or provide other wrappers. In the design of this feature, we have considered adding a way to use GND unsafely, but we’re not sure what the demand will be. Do you need to use GND unsafely? Let me know.
  • In .hs-boot files (see the relevant section of GHC’s user manual), all declarations must match exactly with the declarations in the corresponding .hs file. This includes roles. However, it is acceptable to leave out definitions in a .hs-boot file. By default, roles are guessed to be R in .hs-boot files. If you have an .hs-boot file that declares a datatype or class whose definition is omitted and whose parameters are not at role R, you will have to add a role annotation. I’m hoping this doesn’t come up too often.

Separately from breakage, writers of libraries may also want to think about whether a role annotation would be helpful in their declarations. The best reason I can think of to do this is to prevent users from using GND on a class. For example, a Set uses a type’s Ord instance to order the data internally. But, the definition of Set does not use type families or other features forcing an N role. So, Set’s parameter will be at role R. Yet, if GND is used to lift a class mentioning Set from, say, Int to Age, the Ord instances for Int and Age might be different, and bad behavior will result. Note that this “bad behavior” would not be a type error, just incorrect runtime behavior. (If it were a type error, roles would hopefully stop this from happening!) The upshot of this is that Set’s parameter should be labeled with role N.

Further reading

To learn more about roles in GHC, you can check out the up-to-date wiki pages on the subject, for users and for implementers.

If you run into problems, do let me know!

About these ads

11 thoughts on “Roles: a new feature of GHC

  1. Max Kirllov

    As far as I understand, the reason why the GNDs break Set is that the Set rely on non-exported implementation to keep sorting, and GND break though this isolation.

    Could it be a solution for this problem to forbid GND if constructors of some of the involved datatypes are not visible in the scope?

    Reply
    1. Richard Eisenberg Post author

      You are highlighting a separate problem with GND than the one that roles solve, that GND can break through an abstraction barrier. For example, see http://ghc.haskell.org/trac/ghc/ticket/5498 What you suggest — allowing GND only when the constructor is in scope — would fix this new problem. I don’t have a good enough grasp on how much code such a change would break. I do think that this problem needs to be adequately addressed to allow GND to be considered in the Safe Haskell subset.

      The key point about Set in the original post is that using GND with Set is completely type-safe, just not the right thing to do.

      Reply
      1. Max Kirillov

        I seem to realize that “constructors not in scope” look very similarly for innocent data types, which were not just imported to not clutter the scope, and the types like Set. Maybe not distinguishable at all. At least for reify from TH the Set’s constructors are visible. So the idea is not that good.

        Maybe yes, some explicit declaration that the constructor is “unsafe” would work better.

  2. AntC

    Thank you Richard. When I first read your post, something ‘felt’ wrong but I couldn’t put my finger on it at the time. Apologies that I’ve taken so long to figure it out for myself.
    I’ve gone back to that POPL 2011 paper. The critical step seems to be section 2.1 Coercion lifting where it says “Notationally, we say that `Int ~ Age`, where we use `~` for type equality.” It’s confusing to use `~` there because it is _not_ in the same sense as `~` that can appear in equality constraints. Is this what you mean by “a flaw in the theory”?
    Section 2.1 goes on to explain how “newtype deriving” is implemented by GHC. I kinda expected that “newtype deriving” would be implemented by notionally attaching `deriving (…)` to the newtype decl (where the ellipsis lists every class which the concrete type is an instance of); and then having GHC ‘follow the rules’ for deriving instances (not that those rules are very clearly laid out anywhere ;-). That should at least mean pattern matching on the newtype “data constructor” for each method.
    But what GHC does is merely pretend that every value of the newtype has a constructor. So would it be true to say that in effect GHC for GND produces instances that GHC wouldn’t accept if the programmer had written them ‘by hand’?
    Pinning the blame on GADTs or the “combination” with type families seems to be missing the point: It’s not just that ” type families can tell the difference between Int and Age”; rather: `Int`s _are_different_ to `Age`s and anything that can’t or doesn’t tell the difference is wrong. GHC’s implementation of GND is broken; it was never type safe, even if GHC ‘got away with it’ for years.
    Since Haskell’s type model is nominal typing, we should never have `Age ~ Int`. The fact that those two types happen to have the same memory mapping (in some implementation) should be irrelevant; just as irrelevent as if for some implementation Int, Bool, Char happen to use a 32-bit word.
    My (admittedly folksy) understanding of newtypes is that they are just like [**] declaring a data except that the compiler can produce more efficient code sometimes. But the Coercion lifting seems to turn that upside down: newtypes are more efficient, and can produce type-safe code sometimes ;-).

    So Roles ‘feels’ like a band-aid. Would Roles be needed if GHC derived instances for newtypes ‘properly’ by, errm, generating derived instances for each class individually; then _and_only_then_ optimising the code where it can take advantage of two types happening to share the same memory mapping.?

    [**] leaving aside the edge case of bottoms with the data constructor.

    Reply
    1. Richard Eisenberg Post author

      There are a few points brought up in your post:

      - Q: Does GHC accept instances through GND that could not be written by hand? A: Yes, in GHC 7.6; no, in GHC 7.8. These “out-of-band” instances in GHC 7.6 were exactly the problem with GND. In GHC 7.8, the instances are generated using the new function `coerce.` (See http://www.joachim-breitner.de/blog/archives/610-Adding-safe-coercions-to-Haskell.html) These instances can easily be written by hand.

      - Q: Why blame type families & GADTs? Aren’t newtypes the problem? A: Well, yes. Leaving aside the choice of notation in that paper, the whole idea of newtypes are somewhat anathema to Haskell’s type system. AntC’s suggestion that newtypes should be just like datatypes (ignoring the bit about bottoms) except sometimes more efficient is a good one. The problem is that users want even more than this. Leaving aside the usefulness of GND for a moment, it seems that, if we know that Age and Int are the same under the hood, we should be able to conclude that [Age] and [Int] are the same and be able to convert between these for free. Though this conversion is done by `coerce`, that feature would be nigh inconceivable without the theory of roles underpinning its safety. Through roles, we allow the efficiency gains from newtypes and no longer have to deal with the hole they make in the type system. Are roles a band-aid? Perhaps. But they are necessary if we are to keep newtypes working in convenient ways and in ways that have become popular.

      - Q: Should the instance generation through GND follow the “specifications” for built-in classes? A: I’m not quite sure what you’re asking here. GND allows for the derivation of instances of most classes, including those not generally derivable. That’s because the GND mechanism uses an already-existing instance when building its new one — it doesn’t have to generate code from scratch.

      I hope this helps clarify the point. In short, I agree that, perhaps, roles are fiddly and seem like a strange lump in an otherwise nice and smooth type system. But, this lump powers real efficiency gains in running code that the community have come to depend on.

      Reply
  3. AntC

    (Thanks Richard for the quick reply. Having Roles is a big improvement over GHC’s potential type unsafety at v7.6. I’m not quite sure myself what I’m asking; let me put it like this …)
    For any new feature, it’s a good discipline to describe it in terms of existing functionality. This mental model seems to break down for GND: it ought to be that we can describe the derived instances as if they were hand-written instances, generated by “specifications”. So what worries me in your response to the 3rd Q is “… doesn’t … generate code …”.
    GND using an already-existing instance shortcuts (for the sake of efficiency) the usual compilation and type safety validation.
    I’d prefer to be able to continue with the mental model that GND does generate the instances; and GHC validates/compiles them. And then GHC (in an optimisation pass) spots that the code for `Age` is the same as for `Int` (or that there’s a coercion/unwrap/rewrap that is in effect a null op), so shares the code (and/or eliminates null ops). And that optimisation should be applicable whether the instance was hand-written or GND.

    Reply
  4. Richard Eisenberg Post author

    I’ve been quoted out of context! :)
    The full(er) context is “doesn’t … generate code from scratch.” It *does* just generate code now, as of a few weeks ago. Let’s use a concrete example:

    newtype RestrictedIO a = MkRIO { unRIO :: IO a }
    deriving Monad

    will generate the following

    instance Monad RestrictedIO where
    return = coerce (return :: a -> IO a) :: forall a. a -> RestrictedIO a
    (>>=) = coerce ((>>=) :: IO a -> (a -> IO b) -> IO b) :: forall a b. RestrictedIO a -> (a -> RestrictedIO b) -> RestrictedIO b
    fail = coerce (fail :: String -> IO a) :: forall a. String -> RestrictedIO a

    You can see this by using -ddump-deriv on HEAD. The inner type annotations are necessary to fix the “from” type of the coercion, and the outer type annotations are necessary to bind some scoped type variables. (ScopedTypeVariables is enabled locally when processing the generated definitions. This local extension enabling is not accessible in source Haskell, but I don’t think it should cause too much concern.)

    I’m not sure how satisfying an answer this is, really, because it just pushes the magic out of GND and into coerce. What might be nice about it, though, is that the `coerce` magic is now easily accessible to programmers, so GND doesn’t have special powers that ordinary programmers don’t. (This is a departure from GHC 7.6, where GND has its own particular brand of magic.)

    Reply
  5. AntC

    Ah, here’s a critical case rather than all that speculation and uneasy feeling. Suppose in the BadIdea example we had:
    type instance IsItAgeOrInt Age = Bool — same result as for Int; or even:
    type instance IsItAgeOrInt Age = IsItAgeOrInt Int — blimmin’ obvious
    Then `deriving instance BadIdea Age` could ‘share’ the instance for Int and would be type safe.
    I presume that Roles is still going to reject that GND, because it doesn’t inspect the type family instance(?)
    But if that GND actually generated the instance:
    instance BadIdea Age where frob (MkAge x) = (x > 0)
    GHC could see that the instance is type-correct;
    and see that unwrapping the `MkAge` constructor is a no-op;
    and so see that the code is shareable with the instance for Int.
    (I guess that at v7.8, if I hand-wrote that instance, it would compile OK but I wouldn’t get any code sharing?)
    How about we introduce:
    deriving type instance IsItAgeOrInt Age

    Reply
  6. Richard Eisenberg Post author

    If the type family instances between Age and Int agree, it actually *does* work! This is one of the beauties to be found by basing GND on coerce, which was a later design decision in all of this. The code for the GND’d instance just uses coerce, which does full type inference/reasoning on the types at hand. This includes evaluating type families as far as necessary to show that the types are compatible (or not, as the case may be).

    Just to make sure, I really tried this with HEAD, and it indeed compiles without a hiccup. When I use the type family instances in the original post (where IsItAgeOrInt Age = Char), the error message even says “Could not coerce from ‘Bool’ to ‘Char’”.

    Reply
  7. AntC

    Thanks Richard, that’s terrific!
    It’s just that I’m not seeing how that (desirable) behaviour follows from what it says in the write-up for Roles: the result of `frob` is given by a type family; so that makes it Nominal (non-parametric); so we can’t use GND(??)
    And now you’re saying that GND goes OK; so `coerce` is trying to force type inference; so it’s ignoring Roles(???). Explain again: what’s the, errm, role of Roles? Perhaps it’s for separate compilation where `coerce` can’t do full type inference (can’t see instances defined in other modules)?
    I guess there’s also a lurking question of whether this is achieving any efficiences or sharing of code? (That’s a relatively minor question IMO compared to type safety and predictable semantics.)

    Reply

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s