Injective type families?

[Dan Doel]

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