Re: [isabelle] Parametric theories



On Wed, 11 Apr 2012, Daniel Schoepe wrote:

I'm trying to build a theory that is parametric in some types and
would like to know the recommended way for doing that.

It depends what "parameteric on types" shall mean exactly. Depending on plain type parameters in the manner of schematic polymorphism works quite painlessly, and type inference sorts out things most of the time, without too much explicit type annotations.

In contrast, depending on type *constructors* with their own type arguments does not work within the logic, and requires something like AWE from Bremen.


Use type variables everywhere -- this will get very tiresome very quickly. Locales don't seem to offer a complete way around that either, at least the following does not seem to work:

locale Foo = fixes x :: "'a"
begin
 type_synonym bar = "'a \times 'a"
end

Normally you just refer to 'a, 'b, 'c in your specifications causally (or implicitly), without introducing too many explicit types mentioned in the formal text. So it might not be as tiresome as anticipated, depending on the application.

A type_synonym within a local theory context could be made to work, but it is not so often required in practice to induce significant demands to implement that. Other things are more urgent, sich as datatype and record types within local contexts.


	Makarius





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