Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] HOLCF equality

Email Gateway (Aug 19 2022 at 08:06):

From: Christian Sternagel <c-sterna@jaist.ac.jp>
Dear all,

is there already something like Haskell's "Eq" typeclass for HOLCF
(which seems to be neccessariy/convenient to formalize typical Haskell
functions). If not, are there any other reasons than lack of time?

cheers

chris

Email Gateway (Aug 19 2022 at 08:06):

From: Christian Sternagel <c-sterna@jaist.ac.jp>
When trying to define my own type class (I dropped all axioms for the
sake of a minimal example)

class eq =
fixes eq :: "'a → 'a → tr"

and instantiating the lift type

declare [[names_long]]

instantiation lift :: (type) eq
begin

I obtain

Conflict of type arities for classes Representable.predomain <
Bifinite.profinite:
Lift.lift :: (HOL.type)
Representable.predomain and
Lift.lift :: (Countable.countable)
Bifinite.profinite

which I don't understand. What is happening here?

cheers

chris

Email Gateway (Aug 19 2022 at 08:07):

From: Peter Gammie <peteg42@gmail.com>
Christian,

HOLCF is built out on a series of type classes. The most basic class that supports the continuous function space constructor (->) is "cpo".

So the most general definition for your eq class is:

class eq = fixes eq :: "'a::cpo -> 'a -> tr"

I think you can find some discussion in the archives about what the default class is in HOLCF and why it is hard to get it right for all uses.

cheers
peter

Email Gateway (Aug 19 2022 at 08:07):

From: Brian Huffman <huffman@in.tum.de>
On Sat, Jul 7, 2012 at 6:51 AM, Christian Sternagel
<c-sterna@jaist.ac.jp> wrote:

When trying to define my own type class (I dropped all axioms for the sake
of a minimal example)

class eq =
  fixes eq :: "'a → 'a → tr"

Hi Chris,

Try "print_classes" after this definition, and you will see that class
"eq" has "domain" as a superclass. The reason is that HOLCF declares
class "domain" (consisting of types embeddable into the universal
domain type "udom") as the default sort, so each occurrence of 'a in
the type signature is treated as "'a::domain".

You can override this by re-declaring a different default sort, or
with a sort annotation:

class eq = fixes eq :: "'a::cpo → 'a → tr"

and instantiating the lift type

declare [[names_long]]

instantiation lift :: (type) eq
begin

I obtain

Conflict of type arities for classes Representable.predomain <
                   Bifinite.profinite:
  Lift.lift :: (HOL.type)
    Representable.predomain and
  Lift.lift :: (Countable.countable)
    Bifinite.profinite

which I don't understand. What is happening here?

For type "'a lift" to be in class "domain", type 'a must be in class
"countable".

Now you are attempting to show that type "'a lift" is in class "eq" (a
subclass of "domain") if 'a is in class "type" (a superclass of
"countable").

Such combinations of instances are illegal in Isabelle, because they
would cause problems with principal types for type inference. (I think
the technical term for the requirement is "regularity",
"co-regularity", or something like that.)

If you keep "domain" as a superclass of "eq", then the following
instance for "lift" will work:

instantiation lift :: (countable) eq

• Brian

Email Gateway (Aug 19 2022 at 08:07):

From: Brian Huffman <huffman@in.tum.de>
A library with class "Eq" and other classes from Haskell would
certainly be useful, and I don't think it would take much time to
implement.

I think the main reason I never implemented it is I could never decide
on the details: what to name the functions, what syntax to provide,
what axioms to use, which classes to provide, etc.

• Brian

Email Gateway (Aug 19 2022 at 08:07):

From: Christian Sternagel <c-sterna@jaist.ac.jp>
I am currently using

class eq =
fixes eq :: "'a::pcpo → 'a → tr"
assumes equals_strict [simp]:
"eq⋅x⋅⊥ = ⊥" "eq⋅⊥⋅y = ⊥"
and eq_iff [iff]:
"eq⋅x⋅y = TT ⟷ x ≠ ⊥ ∧ y ≠ ⊥ ∧ x = y"
"eq⋅x⋅y = FF ⟷ x ≠ ⊥ ∧ y ≠ ⊥ ∧ x ≠ y"
"eq⋅x⋅y = ⊥ ⟷ x = ⊥ ∨ y = ⊥"

but did not think much about the details ;).

Maybe something like a theory for standard Haskell functions could be
placed where everybody can browse and contribute? (I am currently mainly
defining very basic list functions and proving basic properties about them.)

cheers

chris

Email Gateway (Aug 19 2022 at 08:08):

From: Brian Huffman <huffman@in.tum.de>
On Mon, Jul 9, 2012 at 11:14 AM, Christian Sternagel
<c-sterna@jaist.ac.jp> wrote:

I am currently using

class eq =
  fixes eq :: "'a::pcpo → 'a → tr"
  assumes equals_strict [simp]:
    "eq⋅x⋅⊥ = ⊥" "eq⋅⊥⋅y = ⊥"
    and eq_iff [iff]:
    "eq⋅x⋅y = TT ⟷ x ≠ ⊥ ∧ y ≠ ⊥ ∧ x = y"
    "eq⋅x⋅y = FF ⟷ x ≠ ⊥ ∧ y ≠ ⊥ ∧ x ≠ y"
    "eq⋅x⋅y = ⊥ ⟷ x = ⊥ ∨ y = ⊥"

but did not think much about the details ;).

I think your eq_iff rules need to be weakened like this:

"eq⋅x⋅y = TT ==> x = y"
"eq⋅x⋅y = FF ==> x ≠ y"

Otherwise instances for lazy lists or other lazy datatypes are not
possible. (Your class "eq" is provably a subclass of "flat".)

Alternatively, a subclass "eq_flat" with the strong eq_iff rules might
be useful alongside a weakened "eq" class.

Maybe something like a theory for standard Haskell functions could be placed
where everybody can browse and contribute? (I am currently mainly defining
very basic list functions and proving basic properties about them.)

This sounds like a good idea. The question is where to put it. We
could add a theory file under HOLCF in the distribution, or we could
add an AFP entry for this purpose. (Maybe using the distribution is
better; as an "archive", the AFP seems not to be intended so much for
dynamic, growing works with open authorship.)

• Brian

Email Gateway (Aug 19 2022 at 08:08):

From: Tobias Nipkow <nipkow@in.tum.de>
The distribution is more lightweight than the AFP. But in either case the set of
people that can add contributions will be restricted.

Tobias

Email Gateway (Aug 19 2022 at 08:08):

From: Makarius <makarius@sketis.net>
After several successful years of AFP, this question is still coming up
routinely, and I wonder myself often.

Can the official AFP editors make some more explicit statements on the AFP
website what it really is? What are the official policies to grow it?
Will new versions of articles replace old ones, keeping the name or
changing the name? Etc. etc.

For example, JinjaThreads seems to have been a perfectly dynamic entry in
all these years, without any archival character beyond the Mercurial
history.

Makarius

Email Gateway (Aug 19 2022 at 08:09):

From: Christian Sternagel <c-sterna@jaist.ac.jp>
On 07/09/2012 10:04 PM, Brian Huffman wrote:

On Mon, Jul 9, 2012 at 11:14 AM, Christian Sternagel
<c-sterna@jaist.ac.jp> wrote:

I am currently using

class eq =
fixes eq :: "'a::pcpo → 'a → tr"
assumes equals_strict [simp]:
"eq⋅x⋅⊥ = ⊥" "eq⋅⊥⋅y = ⊥"
and eq_iff [iff]:
"eq⋅x⋅y = TT ⟷ x ≠ ⊥ ∧ y ≠ ⊥ ∧ x = y"
"eq⋅x⋅y = FF ⟷ x ≠ ⊥ ∧ y ≠ ⊥ ∧ x ≠ y"
"eq⋅x⋅y = ⊥ ⟷ x = ⊥ ∨ y = ⊥"

but did not think much about the details ;).

I think your eq_iff rules need to be weakened like this:

"eq⋅x⋅y = TT ==> x = y"
"eq⋅x⋅y = FF ==> x ≠ y"

Otherwise instances for lazy lists or other lazy datatypes are not
possible. (Your class "eq" is provably a subclass of "flat".)
Thanks for pointing this out. As I said, I did not think much about the
details yet (and my only instance of "eq" was "lift").

Alternatively, a subclass "eq_flat" with the strong eq_iff rules might
be useful alongside a weakened "eq" class.
That sounds reasonable.

Maybe something like a theory for standard Haskell functions could be placed
where everybody can browse and contribute? (I am currently mainly defining
very basic list functions and proving basic properties about them.)

This sounds like a good idea. The question is where to put it. We
could add a theory file under HOLCF in the distribution, or we could
add an AFP entry for this purpose. (Maybe using the distribution is
better; as an "archive", the AFP seems not to be intended so much for
dynamic, growing works with open authorship.)
I would suggest to start with a sourceforge project (or anything
equivalent) until there actually is something constituting a "standard
library" which can then be submitted to the AFP (or the distribution).

• chris

Email Gateway (Aug 19 2022 at 08:09):

From: Tobias Nipkow <nipkow@in.tum.de>
Am 09/07/2012 23:00, schrieb Makarius:

On Mon, 9 Jul 2012, Tobias Nipkow wrote:

Am 09/07/2012 15:04, schrieb Brian Huffman:

Maybe using the distribution is better; as an "archive", the AFP seems not to
be intended so much for dynamic, growing works with open authorship.

The distribution is more lightweight than the AFP. But in either case the set
of people that can add contributions will be restricted.

After several successful years of AFP, this question is still coming up
routinely, and I wonder myself often.

Can the official AFP editors make some more explicit statements on the AFP
website what it really is? What are the official policies to grow it? Will new
versions of articles replace old ones, keeping the name or changing the name?
Etc. etc.

http://afp.sourceforge.net/updating.shtml

For example, JinjaThreads seems to have been a perfectly dynamic entry in all
these years, without any archival character beyond the Mercurial history.

In addition it has a change history which needs to be updated and resides not in
the individual entry but in the central database.

Tobias

Email Gateway (Aug 19 2022 at 08:09):

From: Christian Sternagel <c-sterna@jaist.ac.jp>
On 07/09/2012 10:04 PM, Brian Huffman wrote:

On Mon, Jul 9, 2012 at 11:14 AM, Christian Sternagel
<c-sterna@jaist.ac.jp> wrote:

I am currently using

class eq =
fixes eq :: "'a::pcpo → 'a → tr"
assumes equals_strict [simp]:
"eq⋅x⋅⊥ = ⊥" "eq⋅⊥⋅y = ⊥"
and eq_iff [iff]:
"eq⋅x⋅y = TT ⟷ x ≠ ⊥ ∧ y ≠ ⊥ ∧ x = y"
"eq⋅x⋅y = FF ⟷ x ≠ ⊥ ∧ y ≠ ⊥ ∧ x ≠ y"
"eq⋅x⋅y = ⊥ ⟷ x = ⊥ ∨ y = ⊥"

but did not think much about the details ;).
Btw, the above strictness rules came from observing how ghci handled
equalities involving "undefined". For the case of (==) this is
relatively simple.

On a related note, in the the ghc sources there are often several
versions of a function (usually one due to the Haskell report and an
optimized one). Furthermore there are rewrite rules that can be used by
the compiler. In both cases the strictness-behaviour (I don't know the
correct technical term) is sometimes different, i.e., optimized
functions behave different (I think I experienced this with the two
versions of "any", but am not a 100% sure) from report versions and
sometimes rewrite rules have not been correct when considering
strictness, e.g., consider the following excerpt from the sources:

{-# RULES
"filter" [~1] forall p xs. filter p xs = build (\c n -> foldr
(filterFB c p) n xs)
"filterList" [1] forall p. foldr (filterFB (:) p) [] = filter p
"filterFB" forall c p q. filterFB (filterFB c p) q = filterFB c
(\x -> q x && p x)
#-}

-- Note the filterFB rule, which has p and q the "wrong way round" in
the RHS.
-- filterFB (filterFB c p) q a b
-- = if q a then filterFB c p a b else b
-- = if q a then (if p a then c a b else b) else b
-- = if q a && p a then c a b else b
-- = filterFB c (\x -> q x && p x) a b
-- I originally wrote (\x -> p x && q x), which is wrong, and actually
-- gave rise to a live bug report. SLPJ.

For verification this is of course important. It seems that HOLCF
provides a nice way to verify such compiler rewrite rules in a reliable way.

chris

I think your eq_iff rules need to be weakened like this:

"eq⋅x⋅y = TT ==> x = y"
"eq⋅x⋅y = FF ==> x ≠ y"

Otherwise instances for lazy lists or other lazy datatypes are not
possible. (Your class "eq" is provably a subclass of "flat".)

Alternatively, a subclass "eq_flat" with the strong eq_iff rules might
be useful alongside a weakened "eq" class.

Maybe something like a theory for standard Haskell functions could be placed
where everybody can browse and contribute? (I am currently mainly defining
very basic list functions and proving basic properties about them.)

This sounds like a good idea. The question is where to put it. We
could add a theory file under HOLCF in the distribution, or we could
add an AFP entry for this purpose. (Maybe using the distribution is
better; as an "archive", the AFP seems not to be intended so much for
dynamic, growing works with open authorship.)

• Brian
  

Last updated: Apr 26 2024 at 04:17 UTC