Re: [isabelle] HOLCF equality type class



On Thu, Jul 26, 2012 at 7:05 AM, Christian Sternagel
<c-sterna at jaist.ac.jp> wrote:
> 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)
> - ...

Perhaps you could split eq into two separate classes: One only
requires eq to be an equivalence relation, and the other requires eq
to implement actual equality. You could prove a subclass relation
between the two.

In general, I suppose that a single Haskell class might need to
correspond to a whole collection of Isabelle classes, since there may
be several different sets of possible laws that correspond to the same
set of overloaded functions. It would probably be good to come up with
a standard naming scheme for these kinds of situations.

- Brian

P.S. I'm not sure if we ever advertised your sourceforge project on
the users list, maybe only on the dev list.

Anyway, we are building a collection of libraries for HOLCF in
Isabelle2012; the aim is to formalize many of the functions and type
classes from the Haskell prelude. I encourage anyone interested in
formalizing Haskell programs to have a look!

http://sourceforge.net/p/holcf-prelude/





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