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

Correct. For the "newtype wrapper" stuff you could simply omit a "deriving( NT )" on Set. But the role annotation *also* prevents bogus newtype-deriving, as you are pointing out. Eg class C a where foo :: Set a -> a instance C Int where ... newtype Age = MkAge Int deriving( C ) -- BOGUS deriving Might you or Richard add an example like this to the user manual section? It's far from obvious! Simon | -----Original Message----- | From: Glasgow-haskell-users [mailto:glasgow-haskell-users- | bounces@haskell.org] On Behalf Of Joachim Breitner | Sent: 18 August 2013 18:46 | To: glasgow-haskell-users@haskell.org | Subject: Marking type constructor arguments as nominal (e.g. Set) | | 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