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!

Advertisement