Personal tools

GHC/Coercible

From HaskellWiki

< GHC
Jump to: navigation, search
This page contains additional information about
Coercible
and augments the documentation and the ICFP 2014 paper. This is a feature that first appeared in GHC 7.8.1 and will likely evolve futher.

Contents

1 The problem

Given a newtype

newtype HTML = MkHTML String
we can convert between
HTML
and
String
with
toHTML :: String -> HTML
toHTML s = MkHTML s
 
fromHTML :: HTML -> String
fromHTML (MkHTML s) = s

and these conversions are free, i.e. they have no run-time cost.

But how do we get from
[String]
to
[HTML]
? We can write
toHTMLs :: [String] -> [HTML]
toHTMLs = map MkHTML
but the execution of
map
incurs a cost at run-time.

2 Using Coercible

The solution available since GHC-7.8.1 is to use
coerce
from the module
Data.Coerce
:
import Data.Coerce
toHTMLs :: [String] -> [HTML]
toHTMLs = coerce
It works like
unsafeCoerce
, i.e. has no run-time cost, but the type checker ensures that it really is safe to use it. If you use it illegally like in
wrong :: [Int] -> [Bool]
wrong = coerce

you will get an error message:

    Could not coerce from ‘Int’ to ‘Bool’
      because ‘Int’
          and ‘Bool’
          are different types.
      arising from a use of ‘coerce’
    In the expression: coerce
    In an equation for ‘wrong’: wrong = coerce
The type of
coerce
is
Coercible a b => a -> b
, and the instances of the “type class”
Coercible
(which behaves almost like a regular type class) ensure that
Coercible s t
is only solvable if
s
and
t
have the same run-time representation.

3 Interesting things to note

3.1 Using newtypes internally and externally differently

You can unwrap a newtype using
coerce
only if the corresponding constructor is in scope. This allows you to do free conversions in your own library (where the constructor is in scope), while controlling what others can do using role annotation: This newtype has a phantom parameter, but the role annotation allows users of the library to coerce
NT s
to
NT t
only if
Coercible s t
holds:
newtype NT a = MkNT ()
type role NT representational
Nevertheless, as long as the constructor
MkNT
is in scope, we can do
coerce :: NT Bool -> NT Int
, if we wish to do so.

(This does not yet work in GHC-7.8, as a bug in GHC was fixed only later.)

3.2 Using datatypes internally and externally differently

A similar goal can be achieved for data types, but at a slight expense of convenience. Say you want export data type
Set a
that your users must not coerce freely. The way to go is to add a role annotation
module Set (Set) where
data Set a = ....
type role Set nominal
But then not even you can coerce
Set s
to
Set t
, and you might have valid reasons to do so!

You can solve this by adding a wrapper newtype:

module Set (Set) where
data InternalSet a = ....
newtype Set a = MkSet (InternalSet a)
type role Set nominal
As long as
MkSet
is in scope,
Coercible (Set s) (Set t)
will reduce to
Coercible (InternalSet s) (InternalSet t)
, which – assuming
Set
’s parameter is inferred as representational – reduces to
Coercible s t
as desired. In external code, where
MkSet
is not in scope, the constraint
Coercible (Set s) (Set t)
will not be solvalble – the role annotation on
Set
prevents coercing under it, and the newtype unwrapping cannot be used as
MkSet
is not in scope.

3.3 Recursive newtypes

Recursive newtypes pose a general challenge for GHC's solver for
Coercible
constraints. If all newtype constructors are in scope, the solver sometimes tries to normalize away all occurrences of newtypes and then show that these normal forms are
Coercible
. (If a constructor is not in scope, the solver will not unwrap that newtype.) When a newtype is recursive, this process ends with an error, before GHC loops forever. It is believed that solving
Coercible
constraints in the presence of recursive newtypes is an undecidable problem (see here), and so this behavior is somewhat reasonable. If you need to use
coerce
with recursive newtypes and the solver is failing you, it might be worth thinking a bit about its implementation and working around that. For example, you might need to write a type-restricted synonym for
coerce
in a module that specifically does not import certain constructors, just to control the solver. Of course, if you think that you have an easy case to solve, feel free to post your example in a bug report.