[isabelle-dev] Future of permanent_interpretation

[Clemens Ballarin]

Hi Florian,

this proposal goes too far, of perhaps, not far enough.  Let me explain.

There is of course nothing wrong with providing new commands and enhancements for frequent use cases.  However, I don't see a good reason why users should be forced to write 'permanent_interpretation' where they could write 'interpretation' or 'sublocale'.

I don't object to a careful evolution of the user interface to locales, but I don't think you're heading in the right direction.  Your 'permanent_interpretation' lets users make some definitions followed by, depending on the context, an interpretation or a sublocale declaration.  This is certainly useful, but it is not general enough for making it the preferred command.  For example, it doesn't permit function declarations.  It also blurs the distinction between 'interpretation' and 'sublocale' by calling the latter 'permanent_interpretation' when in a locale context, but not at the level of theories, but instead calling the former 'permanent_interpretation' at the level of theories.

It should be kept in mind that in the current design the 'interpretation' commands are effective for the lifetime of their context: in theories they are therefore permanent, in context blocks they persist for that block and within a proof 'interpret' provides services for that proof.  This is pretty straightforward.  On the other hand, 'locale' and 'sublocale' are theory-level commands that relate a locale to a locale expression (which in both cases becomes a sublocale of the locale).  Their only difference is that 'locale' declares a new locale while 'sublocale' refers to an existing one.  We have allowed the use of 'sublocale' in locale contexts as a notational convenience, but I don't consider it a good idea to further blur the distinction between 'interpretation' and 'sublocale'.  Calling 'sublocale' 'permanent_interpretation' in some contexts and 'sublocale' in others is certainly bad.  The current design is, of course, not cast in stone, but for changing it, there has to be a consistent vision first, so we know where we are heading.

Certainly, your work has partly been inspired by the feeling that the current locale commands only provide the bare basics for manipulating locales.  For example, basing an interpretation or sublocale declaration on definitions is certainly something that could be done in a fancier manner.  The situation is perhaps a bit similar to that of 'axclass' several years ago, where your work on type classes has improved the user experience dramatically.  If you would like to bring locales forward, you might consider developing ideas along those lines.  The required definitions and proofs for an interpretation could for example be collected in a dedicated context in a step-by-step manner similar to that of class instantiation.  Your work also seems to be inspired by the desire to gradually rename 'sublocale' to 'interpretation', which I find surprising, because, compared to classes, 'sublocale' is the direct analogue of 'subclass' and 'interpretation' is the direct analogue of 'instantiation'.

Clemens


On 13 October, 2015 15:13 CEST, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> wrote: 
 
> Recently in private discussion there was the question what the supposed
> future of permanent_interpretation is supposed to be.
> 
> It looks as follows:
> Step 1)
> 	* Put »permanent_interpretation« into Pure directly.
> Step 2)
> 	* Careful revisiting of the documentation to emphasize the presence of
> permanent_interpretation.
> 	* »permanent_interpretation« as leading construct in the distribution
> and the AFP as far as appropriate
> Step 3)
> 	* Discontinue theory-global »interpretation«, which then is just a
> degenerated form of »permanent_interpretation«.
> 	* Discontinue locale-level »sublocale«, which then is just a
> degenerated form of »permanent_interpretation«.
> 
> There will definitely be one release to breath between step 2 and step 3.
> Cheers,
> 	Florian
> 
> -- 
> 
> PGP available:
> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
>