Re: [isabelle] Parametric theories
On Sat, 14.04.2012 22:02, Makarius wrote:
> 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.
Luckily, just ordinary type parameters are needed in my case.
>> 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
> the application.
While I do have only three or four type parameters, I am using
more or less intricate combinations of them quite often, such as
"(('a \<times> 'b) list \<times> ('c \<Rightarrow> 'd)"
Hence I would prefer to have the ability to give these constructs a name
without having to mention the parameters each time again. (I could
construct a type_synonym that needs to be applied to some parameters,
but then I'd still have to write "('a, 'b, 'c, 'd) SomeSynonym").
I guess I'll give using AWE with the current Isabelle version a shot,
and use type_synonyms with parameters if that fails.
Anyway, thanks for your detailed answer!
A related issue I'm curious about: What was the rationale for
introducing typedecl without a straight-forward way to instantiate it?
Being able to define something that has only been declared earlier seems
rather natural to me.
This archive was generated by a fusion of
Pipermail (Mailman edition) and