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

Simon Peyton-Jones simonpj at microsoft.com
Mon Aug 19 10:34:59 CEST 2013


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 at haskell.org] On Behalf Of Joachim Breitner
| Sent: 18 August 2013 18:46
| To: glasgow-haskell-users at 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 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.dehttp://www.joachim-breitner.de/
|   Jabber: nomeata at joachim-breitner.de  • GPG-Key: 0x4743206C
|   Debian Developer: nomeata at debian.org


More information about the Glasgow-haskell-users mailing list