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
