<div dir="ltr">Is the non-injectivity not an issue here because the type family application gets immediately simplified?</div><div class="gmail_extra"><br><br><div class="gmail_quote">On Sun, Aug 18, 2013 at 12:45 PM, Joachim Breitner <span dir="ltr"><<a href="mailto:mail@joachim-breitner.de" target="_blank">mail@joachim-breitner.de</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi,<br>
<br>
now that roles are in HEAD, I could play around a bit with it. They were<br>
introduced to solve the unsoundness of newtype deriving, but there is<br>
also the problem of abstraction: If I define a set type based on an ord<br>
instance, e.g.<br>
<br>
data Set a = Set a -- RHS here just for demonstration<br>
<br>
the I don’t want my users to replace a "Set Int" by a "Set (Down Int)",<br>
even though the latter is a newtype of the former. This can be prevented<br>
by forcing the role of "a" to be Nominal (and not Representational, as<br>
it is by default). What I just noticed is that one does not even have to<br>
introduce new syntax for it, one can just use:<br>
<br>
type family NominalArg x<br>
type instance (NominalArg x) = x<br>
data Set' a = Set' (NominalArg a)<br>
<br>
and get different roles; here the excerpt from --show-iface (is there an<br>
easier way to see role annotations):<br>
<br>
5b7b2f7c3883ef0d9fc7934ac56c4805<br>
data Set a@R<br>
[..]<br>
8e15d783d58c18b8205191ed3fd87e27<br>
data Set' a@N<br>
<br>
The type family does not get into the way, e.g.<br>
<br>
conv (Set a) = Set' a<br>
<br>
works as usual.<br>
<br>
(I now also notice that the parser actually supports role annotations...<br>
but still a nice, backward-compatible trick here).<br>
<br>
Greetings,<br>
Joachim<br>
<span class="HOEnZb"><font color="#888888"><br>
--<br>
Joachim “nomeata” Breitner<br>
<a href="mailto:mail@joachim-breitner.de">mail@joachim-breitner.de</a> • <a href="http://www.joachim-breitner.de/" target="_blank">http://www.joachim-breitner.de/</a><br>
Jabber: <a href="mailto:nomeata@joachim-breitner.de">nomeata@joachim-breitner.de</a> • GPG-Key: 0x4743206C<br>
Debian Developer: <a href="mailto:nomeata@debian.org">nomeata@debian.org</a><br>
</font></span><br>_______________________________________________<br>
Glasgow-haskell-users mailing list<br>
<a href="mailto:Glasgow-haskell-users@haskell.org">Glasgow-haskell-users@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/glasgow-haskell-users" target="_blank">http://www.haskell.org/mailman/listinfo/glasgow-haskell-users</a><br>
<br></blockquote></div><br></div>