Hello,<div>shouldn't the check go the other way? (i.e., if the RHSs unify, then the LHS must be the same). Here is an example:</div><div><br></div><div>-- This function is not injective.</div><div>type instance F a = Int</div>
<div>type instance F b = Int</div><div><br></div><div>Still, Conal's example would not work if we just added support for injective type functions because + is not injective (e.g., 2 + 3 = 1 + 4). Instead, what we'd need to say is that it is injective in each argument separately, which would basically amount to adding functional dependencies to type functions. Perhaps something like this:</div>
<div><br></div><div>type family (a :+: b) ~ c | c b -> a, c a -> b</div><div><br></div><div>This seems like a feature which could be useful.</div><div><br></div><div>-Iavor</div><div>PS: Conal, I have been working on a GHC extension which has direct support for working with natural numbers at the type-level (e.g., + is a built-in type function which supports cancellation and other properties of the normal + operation). I am keen on collecting different ways in which people use type-level naturals to make sure that my implementation supports them (or at least report a decent error). I wasn't sure if the :+ from your example was just meant to illustrate the issue with injectivity, but if you have a use case for type nats, I'd be curious to find out more.</div>
<div><br></div><div><br></div><div><br></div><div><br><div class="gmail_quote">On Mon, Feb 14, 2011 at 3:26 PM, Simon Peyton-Jones <span dir="ltr"><<a href="mailto:simonpj@microsoft.com">simonpj@microsoft.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">Injective type families are a perfectly reasonable idea, but we have not implemented them (yet). The idea would be:<br>
<br>
* You declare the family to be injective<br>
<br>
injective type family T a :: *<br>
<br>
* At every type instance, injectivity is checked. That is, if you say<br>
<br>
type instance T (a,Int) = Either a Bool<br>
<br>
then we must check that every type instance whose LHS unifies with this has the same RHS under the unifying substitution. Thus<br>
<br>
type instance T (a,Bool) = [a] -- OK; does not unify<br>
type instance T (Int,b) = Either Int Bool -- OK; same RHS on (Int,Int)<br>
<br>
<br>
I think it's mainly a question of tiresome design questions (notably do we want a new keyword "injective"? Should it go before "type"?) and hacking to get it all implemented.<br>
<font color="#888888"><br>
Simon<br>
</font><div><div></div><div class="h5"><br>
| -----Original Message-----<br>
| From: <a href="mailto:glasgow-haskell-users-bounces@haskell.org">glasgow-haskell-users-bounces@haskell.org</a> [mailto:<a href="mailto:glasgow-haskell-users-">glasgow-haskell-users-</a><br>
| <a href="mailto:bounces@haskell.org">bounces@haskell.org</a>] On Behalf Of Dan Doel<br>
| Sent: 14 February 2011 23:14<br>
| To: <a href="mailto:glasgow-haskell-users@haskell.org">glasgow-haskell-users@haskell.org</a><br>
| Subject: Re: Injective type families?<br>
|<br>
| On Monday 14 February 2011 5:51:55 PM Daniel Peebles wrote:<br>
| > I think what you want is closed type families, as do I and many others :)<br>
| > Unfortunately we don't have those.<br>
|<br>
| Closed type families wouldn't necessarily be injective, either. What he wants<br>
| is the facility to prove (or assert) to the compiler that a particualr type<br>
| family is in fact injective.<br>
|<br>
| It's something that I haven't really even seen developed much in fancy<br>
| dependently typed languages, though I've seen the idea before. That is: prove<br>
| things about your program and have the compiler take advantage of it.<br>
|<br>
| -- Dan<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>
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>
</div></div></blockquote></div><br></div>