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

[Joachim Breitner]

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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 198 bytes
Desc: This is a digitally signed message part
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20130818/191abfc0/attachment.pgp>