Injective type families are a perfectly reasonable idea, but we have not implemented them (yet). The idea would be: * You declare the family to be injective injective type family T a :: * * At every type instance, injectivity is checked. That is, if you say type instance T (a,Int) = Either a Bool then we must check that every type instance whose LHS unifies with this has the same RHS under the unifying substitution. Thus type instance T (a,Bool) = [a] -- OK; does not unify type instance T (Int,b) = Either Int Bool -- OK; same RHS on (Int,Int) 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. Simon | -----Original Message----- | From: glasgow-haskell-users-bounces@haskell.org [mailto:glasgow-haskell-users- | bounces@haskell.org] On Behalf Of Dan Doel | Sent: 14 February 2011 23:14 | To: glasgow-haskell-users@haskell.org | Subject: Re: Injective type families? | | On Monday 14 February 2011 5:51:55 PM Daniel Peebles wrote: | > I think what you want is closed type families, as do I and many others :) | > Unfortunately we don't have those. | | Closed type families wouldn't necessarily be injective, either. What he wants | is the facility to prove (or assert) to the compiler that a particualr type | family is in fact injective. | | It's something that I haven't really even seen developed much in fancy | dependently typed languages, though I've seen the idea before. That is: prove | things about your program and have the compiler take advantage of it. | | -- Dan | | _______________________________________________ | Glasgow-haskell-users mailing list | Glasgow-haskell-users@haskell.org | http://www.haskell.org/mailman/listinfo/glasgow-haskell-users