14 Feb
2011
14 Feb
'11
6:14 p.m.
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