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

Joachim Breitner <mail <at> joachim-breitner.de>

2013-08-18 20:37:23 GMT

Hi,
not sure – where would injectivity be needed?
Greetings,
Joachim
Am Sonntag, den 18.08.2013, 15:00 -0500 schrieb 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
>
>
>
> _______________________________________________
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users <at> haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
--
--
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