# Difference between revisions of "GHC/Coercible"

(Created page with "This page contains additional information about <hask>Coercible</hask> and augments the [http://hackage.haskell.org/package/base/docs/Data-Coerce.html documentation] and the [...") |
|||

Line 76: | Line 76: | ||

(This does not yet work in GHC-7.8, as [https://ghc.haskell.org/trac/ghc/ticket/9117 a bug] in GHC [https://ghc.haskell.org/trac/ghc/changeset/7e78faf033405bd5f3b6b787343c98e33d767bda/ghc was fixed] only later.) |
(This does not yet work in GHC-7.8, as [https://ghc.haskell.org/trac/ghc/ticket/9117 a bug] in GHC [https://ghc.haskell.org/trac/ghc/changeset/7e78faf033405bd5f3b6b787343c98e33d767bda/ghc was fixed] only later.) |
||

+ | |||

+ | === 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 <hask>Set a</hask> that your users must not coerce freely. The way to go is to add a role annotation |
||

+ | |||

+ | <haskell> |
||

+ | module Set (Set) where |
||

+ | data Set a = .... |
||

+ | type role Set nominal |
||

+ | </haskell> |
||

+ | |||

+ | But then not even you can coerce <hask>Set s</hask> to <hask>Set t</hask>, and you might have valid reasons to do so! |
||

+ | |||

+ | You can solve this by adding a wrapper newtype: |
||

+ | |||

+ | <haskell> |
||

+ | module Set (Set) where |
||

+ | data InternalSet a = .... |
||

+ | newtype Set a = MkSet (InternalSet a) |
||

+ | type role Set nominal |
||

+ | </haskell> |
||

+ | |||

+ | As long as <hask>MkSet</hask> is in scope, <hask>Coercible (Set s) (Set t)</hask> will reduce to <hask>Coercible (InternalSet s) (InternalSet t)</hask>, which – assuming <hask>Set</hask>’s parameter is inferred as representational – reduces to <hask>Coercible s t</hask> as desired. |
||

+ | |||

+ | In external code, where <hask>MkSet</hask> is not in scope, the constraint <hask>Coercible (Set s) (Set t)</hask> will not be solvalble – the role annotation on <hask>Set</hask> prevents coercing under it, and the newtype unwrapping cannot be used as <hask>MkSet</hask> is not in scope. |

## Revision as of 09:23, 20 May 2014

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

## 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.

## 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.

## Interesting things to note

### 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.)

### 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.