Re: [isabelle] HOLCF equality



On Sat, Jul 7, 2012 at 6:51 AM, Christian Sternagel
<c-sterna at 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





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