# Notes (TLPH 08/15): Roles

# 8.1 Coercions

Since `newtype`

s only differ in the type-system and not in their runtime representation, we can use a proof that types `a`

and `b`

have the same runtime representation to teach the type-system to convert between types `a`

and `b`

. These proofs are automatically generated by the compiler whenever we declare a `newtype`

, and are not allowed to be manually written (there are other mechanisms for manually defining propositional type equality, like in `Type.Reflection`

)

# 8.2 Roles

There are three varieties of roles, in order from strongest to weakest:

- Nominal,
`a ~ b`

- Representational,
`Coercible a b`

- Phantom,
`forall a b. Coercible (Proxy a) (Proxy b)`

There are three inference rules for roles:

- All type parameters are at least
`phantom`

`a -> b`

is`representational`

in`a`

and`b`

(data constructors use`->`

)`a ~ b`

is`nominal`

in`a`

and`b`

, (GADTs, typefamilies use`~`

)

## Exercise 8.2 (i)

`representational a`

, `representational b`

## Exercise 8.2 (ii)

`phantom a`