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

[Florian Haftmann]

Hi Brian,

first of all, your report has indeed exposed a flaw in the processing of
class declarations which has been corrected in
http://isabelle.in.tum.de/repos/isabelle/rev/eddda8e38360,

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

> 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.

	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- 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>