roles

Composable, class-based roles.

Table of contents

• Motivation: What is the cost of a newtype?
• Background
  • The magical Coercible class
  • Lifting coercions
  • Roles to the rescue
• The roles library
  • What problem does this library solve?
  • How can I use this library?
  • History

What is the cost of a newtype?

The conventional wisdom is that Haskell's newtype gives you a zero-cost abstraction--wrapping and unwrapping of newtypes are purely a compile-time operation. Unfortunately, this is not quite the case:

-- A zero-cost abstraction... or is it?
newtype User = User String

-- 'name x' and 'x' will refer to the same in-memory entity at run-time...
name :: User -> String
name (User x) = x

-- ...but 'maybeName x' and 'x' will not be the same at run-time:
-- a new value of type 'Maybe String' is allocated, despite being
-- identical to the input!
maybeName :: Maybe User -> Maybe String
maybeName = fmap name

See the POPL '11 paper Generative Type Abstraction and Type-level Computation for a more through investigation of the problem and a solution, and the ICFP '14 paper Safe Zero-cost Coercions for Haskell for implementation of the Coercible typeclass in Haskell. Still more information can be found on the Haskell wiki.

Background

The magical Coercible class

The solution described in the second paper was to introduce a typeclass Coercible a b of the form

class Coercible a b where
    coerce :: a -> b

There is something a bit magical about a typeclass like this, that requires baked-in compiler support: Consider a declaration newtype New = MkNew Old. Within the module where New is defined, we should be able to freely coerce between New and Old. But then again, if MkNew is not exported, then outside of the module we should not be able to coerce between New and Old. As a result, the Coercible class must involve special compiler magic to ensure that coerce is only available in the appropriate modules.

Lifting coercions

Let's revisit the maybeName issue. Ideally, we would like to rewrite the example to make the coercions explicit, to guarantee zero runtime cost:

newtype User = User String

name :: User -> String
name = coerce

-- GHC knows that it can coerce 'User' to 'String', but
-- how about 'Maybe User' to 'Maybe String'?
maybeName :: Maybe User -> Maybe String
maybeName = coerce

For this to work, we would need instances of Coercible User String (provided by GHC compiler magic, since we're in the module where User is defined) and also Coercible a b => Coercible (Maybe a) (Maybe b).

You might expect GHC could implement a generic "coercion lifting" rule of the form Coercible a b => Coercible (f a) (f b). Unfortunately this would be unsound in the presence of type families:

newtype User = MkUser String

type family Fam
type instance Fam String = Int
type instance Fam User   = Double

If GHC naively added the coercion lifting rule, then we would be able to coerce from Double to Int by:

Coercible User String => Coercible (Fam User) (Fam String) -- a.k.a. Coercible Double Int!

This is obviously no good.

Roles to the rescue

It seems that sometimes we can lift a Coercion a b to a Coercion (f a) (f b) (e.g. for Maybe) and sometimes we cannot (e.g. for Fam). To figure out when a coercion a -> b can be lifted to a coercion f a -> f b, GHC infers a role for the type parameter of f. If f can safely support coercion-lifting, then we say f's type parameter has a representational role; otherwise, it has a nominal role.

Happily, GHC will infer that Maybe's type parameter is representational, while Fam's type parameter is nominal. This lets our definition maybeName = coerce pass the compiler, while attempting to coerce an Int to a Double via Fam will fail.

The roles library

What problem does this library solve?

Unfortunately, in GHC Haskell there is currently (circa late 2017) no way to write something like this:

coerceFirst :: (Coercible a b, Functor f) => [f a] -> Maybe (f b)
coerceFirst []    = Nothing
coerceFirst (x:_) = Just (coerce x)
{- GHC says:
    • Couldn't match representation of type ‘f a’ with that of ‘f b’
        arising from a use of ‘coerce’
      NB: We cannot know what roles the parameters to ‘f’ have;
        we must assume that the role is nominal
-}

GHC rightly refuses to lift the coercion from a to b into a coercion from f a to f b: it does not have any assurance that the functor f uses its type parameter representationally.

In other words, this function needs to have a constraint Representational f that means something like "f's type parameter has a representational role."

This library simply provides the Representational typeclass for a variety of types in base and containers.

How can I use this library?

Since it is not made up of GHC pixie-dust magic, Representational needs a way to convince GHC that the lifted coercion is allowed. It does this via the lone function of the Representational class:

class Representational f where
  rep :: Coercion a b -> Coercion (f a) (f b)

A value of type Coercion a b is like a certificate that tells GHC "you are allowed to coerce a to b". You cash the certificate in by using coerceWith, yielding an actual coercion from a to b. The rep function simply converts a certificate for coercing a to b into a certificate for coercing f a into f b.

We can now fix the example from the previous section:

coerceFirst :: (Coercible a b, Representational f, Functor f) => [f a] -> Maybe (f b)
coerceFirst []    = Nothing
coerceFirst (x:_) = Just (coerceWith (rep Coercion) x)
--                        ~~~~~~~~~~~~~~~~~~~~~~~~~
--                                   |
--   This means: (1) Get a certificate verifying that we can coerce `a` to `b`.
--                   This certificate is `Coercion`, and we got it by making use
--                   of the constraint `Coercible a b`.
--               (2) Since `f` is `Representational`, we can use `rep` to upgrade
--                   the certificate to a certificate for coercion from `f a` to `f b`.
--               (3) Use `coerceWith` to hand the certificate over to GHC, obtaining
--                   an actual coercion from `f a` to `f b` in return.

{- GHC says: sounds good to me! -}

For another usage example, see the withRecMap function from justified-containers, and the corresponding test case. A Representational constraint is used to ensure that large maps are not duplicated in memory, despite undergoing a complex series of newtype-related manipulations. An earlier version of withRecMap worked by fmapping newtype wrappers and unwrappers, which caused an accidental duplication of the map.

History

This package is a fork of Edward Kmett's original roles 0.1. It offers fewer instances of Representational, in exchange for a much smaller set of dependencies. The instances that involve new and eta have been removed, and instances for containers have been added.