Re: [isabelle] HOLCF equality type class
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.
- 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
What do you think?
This archive was generated by a fusion of
Pipermail (Mailman edition) and