Injective type families?

Dan Doel dan.doel at
Tue Feb 15 00:14:10 CET 2011

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

More information about the Glasgow-haskell-users mailing list