Injective type families?
dan.doel at gmail.com
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.
More information about the Glasgow-haskell-users