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
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"
type_synonym bar = "'a \times 'a"
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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and