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"
>> 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.

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 MHonArc.