[isabelle-dev] Local Specification Mechanisms: Brief Experience Report

[Florian Haftmann]

Hi Tjark,

some comments in addition to Clemens':

> * The documentation for local specification mechanisms is not very
> homogeneous.  The tutorials on type classes and locales are valuable.
>>From a user's perspective, however, a unifying discussion (with guidance
> on when to use which) is missing.  (This is probably a natural
> consequence of the fact that Isabelle's local specification mechanisms
> were developed by several people and over a long period of time.)

This is a typical tendency in Isabelle that it is well documented *what*
you can do but to a less extent *how* you actually make use of it;  this
can usually be found implicitly in some typical examples in the
distribution, and the initiate knowledge is where exactly to look at.
Maybe the reason is that people are always too busy to write down such
things (no apologize).

> * "Duplicate parameter(s) in superclasses", as in
> 
>   class A = fixes x :: 'a
>   class B = fixes x :: 'a
>   class C = A + B
> 
> are disallowed.  The usual work-around (I believe) is to introduce a
> syntactic super-class X that fixes the duplicate parameter:
> 
>   class X = fixes x :: 'a
>   class A = X
>   class B = X
>   class C = A + B
> 
> This is artificial when compared to common mathematical practice, and it
> means that one must anticipate the entire class hierarchy whenever one
> introduces fixed parameters.

This was a deliberate choice for the sake of simplicity.  The
correspondence between classes and class parameters is so essential that
it should not be blurred;  this introduces some »globality«, but to some
extent this is always the case with type classes, e.g. there is at most
one instance for each class / type constructor pair.

> * Class assumptions must mention the class type: e.g.,
> 
>   class X = fixes x::'a assumes True
> 
> is rejected because there is "No type variable in part of specification
> element."  Is there a technical reason for this requirement?

Indeed that makes life a lot easier.  For conceptual reasons a class
specification as a whole must refer to exactly one type parameter
(otherwise the canonical interpretation won't work), and breaking this
restriction down to each part of a class specification facilitates
processing.

Hope this helps,
	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://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20101217/d4fc048f/attachment.sig>