*To*: Christian Sternagel <c-sterna at jaist.ac.jp>*Subject*: Re: [isabelle] HOLCF equality type class*From*: Brian Huffman <huffman at in.tum.de>*Date*: Thu, 26 Jul 2012 08:28:59 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <5010D027.2050803@jaist.ac.jp>*References*: <4FF7B559.4010204@jaist.ac.jp> <CAAMXsia+HxapVm_nR9040QGcWKbDJX8SWnaRjLvpPYqnj8YdmQ@mail.gmail.com> <4FFAA0E2.3090006@jaist.ac.jp> <CAAMXsiZQjMH74qEMb0Xn4sNPxr1L3Ho3U9H=t5uPfvh_rb-aeQ@mail.gmail.com> <4FFBBBD4.10706@jaist.ac.jp> <5010D027.2050803@jaist.ac.jp>

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/

**References**:**[isabelle] HOLCF equality***From:*Christian Sternagel

**Re: [isabelle] HOLCF equality***From:*Brian Huffman

**Re: [isabelle] HOLCF equality***From:*Christian Sternagel

**Re: [isabelle] HOLCF equality***From:*Brian Huffman

**Re: [isabelle] HOLCF equality***From:*Christian Sternagel

**Re: [isabelle] HOLCF equality type class***From:*Christian Sternagel

- Previous by Date: Re: [isabelle] Simple question about theory parameter
- Next by Date: Re: [isabelle] Proving cardinality
- Previous by Thread: Re: [isabelle] HOLCF equality type class
- Next by Thread: Re: [isabelle] HOLCF equality type class
- Cl-isabelle-users July 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list