Email Gateway (Aug 19 2022 at 07:55): Email Gateway (Aug 19 2022 at 07:55):From: Christian Sternagel <c-sterna@jaist.ac.jp>
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
Email Gateway (Aug 19 2022 at 07:55):From: Brian Huffman <huffman@in.tum.de>
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.
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/
Email Gateway (Aug 19 2022 at 07:56):From: Joachim Breitner <breitner@kit.edu>
Hi,
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
signature.asc
Last updated: Apr 25 2024 at 20:15 UTC