I think what you want is closed type families, as do I and many others :) Unfortunately we don't have those.<br><br><div class="gmail_quote">On Mon, Feb 14, 2011 at 10:02 PM, Conal Elliott <span dir="ltr"><<a href="mailto:conal@conal.net">conal@conal.net</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">Yes, it's one things that data families do. Another is introducing *new* data types rather than reusing existing ones. - Conal<div>
<div></div><div class="h5"><br><br><div class="gmail_quote">On Mon, Feb 14, 2011 at 1:41 PM, John Meacham <span dir="ltr"><<a href="mailto:john@repetae.net" target="_blank">john@repetae.net</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0pt 0pt 0pt 0.8ex;border-left:1px solid rgb(204, 204, 204);padding-left:1ex">Isn't this what data families (as opposed to type families) do?<br>
<br>
John<br>
<div><div></div><div><br>
On Mon, Feb 14, 2011 at 1:28 PM, Conal Elliott <<a href="mailto:conal@conal.net" target="_blank">conal@conal.net</a>> wrote:<br>
> Is there a way to declare a type family to be injective?<br>
><br>
> I have<br>
><br>
>> data Z<br>
>> data S n<br>
><br>
>> type family n :+: m<br>
>> type instance Z :+: m = m<br>
>> type instance S n :+: m = S (n :+: m)<br>
><br>
> My intent is that (:+:) really is injective in each argument (holding the<br>
> other as fixed), but I don't know how to persuade GHC, leading to some<br>
> compilation errors like the following:<br>
><br>
> Couldn't match expected type `m :+: n'<br>
> against inferred type `m :+: n1'<br>
> NB: `:+:' is a type function, and may not be injective<br>
><br>
> I realize that someone could add more type instances for (:+:), breaking<br>
> injectivity.<br>
><br>
> Come to think of it, I don't know how GHC could even figure out that the two<br>
> instances above do not overlap on the right-hand sides.<br>
><br>
> Since this example is fairly common, I wonder: does anyone have a trick for<br>
> avoiding the injectivity issue?<br>
><br>
> Thanks, - Conal<br>
><br>
</div></div>> _______________________________________________<br>
> Glasgow-haskell-users mailing list<br>
> <a href="mailto:Glasgow-haskell-users@haskell.org" target="_blank">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>
</blockquote></div><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>