Re: [isabelle] locales and 'types'



On Tue, 13 Jul 2010, Peter Gammie wrote:

I find this reasoning a bit confusing for "types" as 'a cannot be used in the RHS anyway, i.e. this is illegal too:

locale X =
 fixes a :: "'a"
begin

types Type = "'a set"

It is not a construct that copes with things that are already fixed in a context.

You can consider this limitation as an accidental feature of the current implementation. Trying a bit harder in the internal structures, one could support type parameters on the RHS one day. It is a very important principle to base a system on assumptions that are as weak as possible, to leave room for continued unfolding of the concepts behind it. Exploiting the inability for type parameters on the RHS now would limit the future growth of the system.


One more note on the example above. In order to avoid unnecessary confusion and unexpected problems, it is important to stick to established Isabelle naming conventions:

* Theory names: capitalized words, typically describing the main concept
   in singular, e.g. "theory Foo_Bar_Concept"

 * Almost everything else in lower case, especially locale and type
   names.

 * Exceptions: capitalized datatype constructors, also some term
   constructions according to typical mathematical usage (e.g. capital
   singleton letters A, B, C, or occasional Foo for "sets" etc.)

Could I humbly suggest that these and other style rules be put in a document that accompanies the distribution?

I promise to mention something like that in the next tutorial on Isar that should come forward this year.

On the other hand we have a bit too many manuals that are often in an inconsistent state, while many things that I find myself explaining again and again are written in the "reference manuals" collection -- these 3 are in fact mostly up to date: isar-ref, implementation, system.

Maybe the next generation of user interfaces needs to tell users directly about thing that are better avoided, or point to relevant sections of the manuals via formal references in the text.


	Makarius






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