illissius at gmail.com
Tue Jan 15 09:48:54 CET 2013
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
This is what Simon's paper 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
"Generative Type Abstraction and Type-level Computation"
Your ship was destroyed in a monadic eruption.
More information about the Glasgow-haskell-users