Injective type families?

[Simon Peyton-Jones]

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 at haskell.org [mailto:glasgow-haskell-users-
|  bounces at haskell.org] On Behalf Of Dan Doel
|  Sent: 14 February 2011 23:14
|  To: glasgow-haskell-users at 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 at haskell.org
|  http://www.haskell.org/mailman/listinfo/glasgow-haskell-users