Marc Weber wrote:
I remembered correctly: The wiki talks about it:
http://www.impredicative.com/wiki/index.php/Disjointness_fun_-_creating_records_using_type_level_functions
quote "
Constructing a record type taking two names and two types. Because
disjointness can't be proofed at type level it must be done at
expression level.
"
My goal was to write a type level projection function - but looks like I
can't do it for this reason.
I don't think there's a good way to implement "type-level projection"
from records. If you share some of the context where you want to use
such an operation, I may be able to suggest an alternate idiomatic
technique.
_______________________________________________
Ur mailing list
[email protected]
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
