[isabelle-dev] type errors when defining subclasses of HOLCF type classes

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Tue Oct 26 15:18:57 CEST 2010

Hi Brian,

first of all, your report has indeed exposed a flaw in the processing of
class declarations which has been corrected in

Unfortunately, the processing of class declarations is notoriously
difficult, especially if the infamous "base sort" is something else than

> class foo = cpo +
>   fixes foo :: "'a → 'a"
> class bar = foo + pcpo +
>   assumes "foo⋅⊥ = ⊥"

The main issue is that ⊥ is just "global" as ⊥::pcpo;  for be able to
cope with such class specification may feature a specific "base sort":

> class foo =
>   fixes foo :: "'a → 'a"
> class bar =
>   assumes "foo⋅⊥ = (⊥::'a::{foo, pcpo})"

But is extremely difficult if not impossible to mix base-sort-based
inheritance with the regular class inheritance.  If ⊥ would exist in a
local variant in class pcpo, you would just write:

> class foo = cpo +
>   fixes foo :: "'a::type → 'a"
> class bar = foo + pcpo +
>   assumes "foo⋅(⊥'a::::type) = ⊥"

I admit that the class command comes with a strong assumption that users
develop their specifications locally if they want refer to them in class
specifications and if not the old-style axclass sometimes appeared more
leigthweight.  However additional options etc. emulating this old
behaviour complicate the whole matter notoriously.




PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20101026/a95f47ed/attachment.asc>

More information about the isabelle-dev mailing list