Re: [isabelle] HOLCF equality type class


Am Donnerstag, den 26.07.2012, 14:05 +0900 schrieb Christian Sternagel:
> Dear all,
> currently we have:
>    "eq⋅x⋅y = TT ⟹ x = y"
>    "eq⋅x⋅y = FF ⟹ x ≠ y"
>    "eq⋅x⋅⊥ = ⊥"
>    "eq⋅⊥⋅y = ⊥"
> After giving this some thought I think that the first rule is 
> problematic since it does only hold for 'eq' instances that implement 
> syntactic equality. I guess all standard and 'deriving' instances of Eq 
> in Haskell implement syntactic equality. However, it might be useful for 
> a programmer to compare 'normalized' values for some types (e.g., data 
> Frac = Frac Int Int). With our current definition this is not possible. 
> We could
> - disallow instances of eq which do not implement syntactic equality 
> (but that is rather restrictive on all functions using 'eq')
> - parametrize eq by some equivalence relation (which would be (=) for 
> many instances)
> - ...

some wildly-used instances like the one for lazy bytestrings do not
implement syntactic equality:

Bytestrings itself might not be formalized soon in your project, but it
is a point towards the equivalence relation parametrized variant.


Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter

Attachment: signature.asc
Description: This is a digitally signed message part

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.