Re: [isabelle] HOLCF equality type class



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)
- ...

What do you think?

cheers

chris





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