[Ur] MY_ORD = resolving eq class instance / functor?

Adam Chlipala adamc at impredicative.com
Tue Nov 29 08:16:53 EST 2011


Marc Weber wrote:
> Excerpts from Adam Chlipala's message of Mon Nov 28 23:57:50 +0100 2011:
>    
>> No, it would be a pair of values, like
>>       eq a * (a ->  a ->  bool)
>> or perhaps a record would be nicer.
>>      
> Does it make a difference passing a ->  b or (a * b) or {A = a, B = b} ?
> For readability only?
>    

I'm not sure what you're asking.  The first type you give clearly allows 
very different operations from the second two, while the second two are 
isomorphic to each other (after desugaring, both are record types, 
differing only in their field names).



More information about the Ur mailing list