Is the non-injectivity not an issue here because the type family
application gets immediately simplified?
On Sun, Aug 18, 2013 at 12:45 PM, Joachim Breitner wrote: Hi, now that roles are in HEAD, I could play around a bit with it. They were
introduced to solve the unsoundness of newtype deriving, but there is
also the problem of abstraction: If I define a set type based on an ord
instance, e.g. data Set a = Set a -- RHS here just for demonstration the I don’t want my users to replace a "Set Int" by a "Set (Down Int)",
even though the latter is a newtype of the former. This can be prevented
by forcing the role of "a" to be Nominal (and not Representational, as
it is by default). What I just noticed is that one does not even have to
introduce new syntax for it, one can just use: type family NominalArg x
type instance (NominalArg x) = x
data Set' a = Set' (NominalArg a) and get different roles; here the excerpt from --show-iface (is there an
easier way to see role annotations): 5b7b2f7c3883ef0d9fc7934ac56c4805
data Set a@R
[..]
8e15d783d58c18b8205191ed3fd87e27
data Set' a@N The type family does not get into the way, e.g. conv (Set a) = Set' a works as usual. (I now also notice that the parser actually supports role annotations...
but still a nice, backward-compatible trick here). Greetings,
Joachim --
Joachim “nomeata” Breitner
mail@joachim-breitner.de • http://www.joachim-breitner.de/
Jabber: nomeata@joachim-breitner.de • GPG-Key: 0x4743206C
Debian Developer: nomeata@debian.org _______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users