[isabelle-dev] Proposing extensions to the Isabelle library?
coglio at kestrel.edu
Sun Dec 16 08:53:12 CET 2012
Hi Florian, thank you for your answer. I understand.
Is there any plan to make things in the library more uniform (one way or
the other)? Is there a preference for new type classes should be
developed (purely syntactic or with assumptions)?
Personally, I like syntactic classes because they are more modular. For
example, in the library extensions that I sent the other day, the
definition of type class finite_lattice_complete would be perhaps
slightly cleaner if bot and top were syntactic classes like Inf and Sup.
Just my 2 cents.
On 12/15/12 2:18 AM, Florian Haftmann wrote:
> Hi Alessandro,
>> On a semi-related topic, I was wondering why the Isabelle library has
>> syntactic type classes for many (most?) operators but not for bot and top.
> this is mainly a result of historic developments and compromises.
> Especially the long-standing operators plus, times etc. have been merely
> syntactic right from the beginning – in lack of type »class«es as they
> are today, there was barely any other choice. Operators added later on
> often were not purely syntactic.
> An advantage of syntactic type classes is that they allow to reuse
> (infix) syntax without reference to particular semantic properties. A
> disadvantage is that they allow to write down things which to the naive
> user appear more specific then they are. E.g. »a + b = b + a«, does not
> hold necessarily, unlike in typical notation in algebra where + is
> always commutative. A similar joke has been "2 + 2 = 4", which was not
> true in general before Isabelle2012. But note that min/max is defined
> purely syntactically, which can also lead to surprises.
> Hope this helps,
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 3735 bytes
Desc: S/MIME Cryptographic Signature
More information about the isabelle-dev