Marking type constructor arguments as nominal (e.g. Set)

[Nicolas Frisby]

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
> 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 at R
>         [..]
>         8e15d783d58c18b8205191ed3fd87e27
>           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).
>
> Greetings,
> Joachim
>
> --
> 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
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20130818/7304871e/attachment.htm>