Marking type constructor arguments as nominal (e.g. Set)
nicolas.frisby at gmail.com
Sun Aug 18 22:00:31 CEST 2013
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 <mail at joachim-breitner.de
> 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):
> data Set a at R
> data Set' a at 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).
> Joachim “nomeata” Breitner
> mail at joachim-breitner.de • http://www.joachim-breitner.de/
> Jabber: nomeata at joachim-breitner.de • GPG-Key: 0x4743206C
> Debian Developer: nomeata at debian.org
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users at haskell.org
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Glasgow-haskell-users