On Tue, Jan 15, 2013 at 3:15 AM, Iavor Diatchki <iavor.diatc...@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. _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
