<div dir="ltr">Non-injectivity of type families sometimes hinders type inference. Consider<div><br></div><div>> Set' (Set.singleton 'c')</div><div class="gmail_extra"><br></div><div class="gmail_extra">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.</div>
<div class="gmail_extra"><br></div><div class="gmail_extra">… 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</div>
<div class="gmail_extra"><br><div class="gmail_quote">On Sun, Aug 18, 2013 at 3:37 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>
not sure – where would injectivity be needed?<br>
<br>
Greetings,<br>
Joachim<br>
<br>
Am Sonntag, den 18.08.2013, 15:00 -0500 schrieb Nicolas Frisby:<br>
<div class="HOEnZb"><div class="h5">> Is the non-injectivity not an issue here because the type family<br>
> application gets immediately simplified?<br>
><br>
><br>
> On Sun, Aug 18, 2013 at 12:45 PM, Joachim Breitner<br>
> <<a href="mailto:mail@joachim-breitner.de">mail@joachim-breitner.de</a>> wrote:<br>
> Hi,<br>
><br>
> now that roles are in HEAD, I could play around a bit with it.<br>
> They were<br>
> introduced to solve the unsoundness of newtype deriving, but<br>
> there is<br>
> also the problem of abstraction: If I define a set type based<br>
> 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<br>
> (Down Int)",<br>
> even though the latter is a newtype of the former. This can be<br>
> prevented<br>
> by forcing the role of "a" to be Nominal (and not<br>
> Representational, as<br>
> it is by default). What I just noticed is that one does not<br>
> 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<br>
> (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<br>
> annotations...<br>
> but still a nice, backward-compatible trick here).<br>
><br>
> Greetings,<br>
> Joachim<br>
><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>
><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>
><br>
><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>
--<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>
</div></div><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></div>