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

[Nicolas Frisby]

Non-injectivity of type families sometimes hinders type inference. Consider

> Set' (Set.singleton 'c')

Naively, we only know that (Char ~ NominalArg a). Since type families are
not necessarily injective, this usually means we cannot determine the type
variable `a' from this constraint. However, since the NominalArg instance
is parametric in `a', I suspect GHC might successfully infer (Char ~ a) in
this case.

… A quick ghci test confirms that GHC does infer (Char ~ a) here. I
apologize for not just experimenting in the first place, but maybe this
email will save someone slightly more time than is required to read it. :P

On Sun, Aug 18, 2013 at 3:37 PM, Joachim Breitner
<mail at joachim-breitner.de>wrote:

> 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
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20130818/750d50ec/attachment.htm>