Notes (TLPH 08/15): Roles

8.1 Coercions

Since newtypes 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