On Sun, 5 Aug 2012, Konrad Slind wrote:
> My opinion is that Peter Homeier's HOL-Omega is the right setting to
> properly implement something locale-like, since it provides
> quantification over type variables in the logic. In plain old HOL the
> implementation of locales as essentially assumptions on goals is too
> limiting for polymorphism.
In the 1.5 decades refining Isabelle locales, we have separated these two
concerns: (1) management of local contexts and definitional specifications
wrt. local contexts, (2) logical foundations for building actual abstract
contexts.
(1) is the infrastructure, consisting of quite a bit of abstract
non-sense. It is now called "local theory" in Isabelle. It provides some
interfaces for definitions in a local context, where the results are
polymorphic in the sense of Hindley-Milner, but some types may remain
fixed according to the context.
(2) are concrete implementations of locales, type classes, type-class
instantiation, unrestricted overloading etc. This could cover other
concepts for modular theories using facilities of HOL-Omega, or external
theory interpretation as in Isabelle/AWE from Bremen.
Both (1) and (2) are difficult to implement. We are still working on
various fine points concerning local syntax (via notation or abbreviation)
that moves between such local contexts. Another challenge that I have
boldly revisited this year is to allow nesting of locale-like contexts.
What is also difficult to get right are declarations for proof tools
associated with theorems produced in abstract situations, when they start
moving around to other contexts. E.g. ways to manage "simpset"-like
containers in conformance to abstract theories and their interpretations
by concrete instances.
Type classes have turned out an important special case for all that,
because the abstraction looks "concrete", via polymorphic constants with
some specific type constraints. Syntax and tool declarationas are often
stable wrt. type-instantiation of class constants, without further ado.
Makarius
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
