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

18 Aug 2013

      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
 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@R
                [..]
                8e15d783d58c18b8205191ed3fd87e27
                  data Set' a@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@joachim-breitner.de • http://www.joachim-breitner.de/
          Jabber: nomeata@joachim-breitner.de  • GPG-Key: 0x4743206C
          Debian Developer: nomeata@debian.org
_______________________________________________
        Glasgow-haskell-users mailing list
        Glasgow-haskell-users@haskell.org
        http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
-- 
Joachim “nomeata” Breitner
  mail@joachim-breitner.de • http://www.joachim-breitner.de/
  Jabber: nomeata@joachim-breitner.de  • GPG-Key: 0x4743206C
  Debian Developer: nomeata@debian.org