Re: [isabelle] HOLCF equality type class



Hi,

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:
http://hackage.haskell.org/packages/archive/bytestring/latest/doc/html/src/Data-ByteString-Lazy.html#line-245

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

Greetings,
Joachim

-- 
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.info.uni-karlsruhe.de/~breitner

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



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