Newtype wrappers

[Gábor Lehel]

On Tue, Jan 15, 2013 at 3:15 AM, Iavor Diatchki
<iavor.diatchki at gmail.com> wrote:
> In general, I was never comfortable with GHC's choice to add an axiom
> equating a newtype and its representation type, because it looks unsound to
> me (without any type-functions or newtype deriving).
> For example, consider:
>
> newtype T a = MkT Int
>
> Now, if this generates an axiom asserting that `froall a. T a ~ Int`, then
> we can derive a contradiction:
>
> T Int ~ Int ~ T Char, and hence `Int ~ Char`.
>
> It looks like what we need is a different concept: one that talks about the
> equality of the representations of types, rather then equality of the types
> themselves.
>
> -Iavor

This is what Simon's paper[1] referenced from the wiki is about,
except he uses the terminology "the representations of types" ->
"types", "the types themselves" -> "codes". (IMHO talking about
"representations" and "types", respectively, would be more
accessible.)

[1] http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/
"Generative Type Abstraction and Type-level Computation"


-- 
Your ship was destroyed in a monadic eruption.