Re: [isabelle] Type parameters in a locale? Datatypes in a locale?
On Fri, 24 Jun 2011, Randy Pollack wrote:
In the locale context I want to define a datatype
datatype ('a,'b) expr = ...
where 'a and 'b are the type variables of the locale, and 'a is the
lattice. It seems that datatype definitions are not accepted in a
locale context, so I defined ('a,'b) expr before the locale and tried
to instantiate it with 'a and 'b inside the locale.
type_synonym exp = "('a,'b) expr"
This fails: '*** Extra variables on rhs: "'b", "'a"'. In my mind, the
type variables 'a and 'b are somehow fixed in the locale context, so
are not extra variables on rhs.
I try something else:
type_synonym ('a,'b) exp = "('a,'b) expr"
This fails too: '*** Locally fixed type arguments "'a", "'b" in type
declaration "exp"' So Isabelle also thinks 'a and 'b are fixed in the
Conceptually, the "locality" of type specifications is limited: it may not
depend on the context parameters. Its own parameters are considered fresh
abstractions, so an accidental clash with outer ones is an error.
type_synonym, typedecl, typedef already work in that sense, but datatype
is still not "localized". (It is on the agenda with high priority for
quite a few years already, although it is become some kind of running
gag in the meantime).
That is, in any (concrete?) instance of the locale 'a and 'b will be
fixed, so I should be able to give them symbolic names and use them as
if they were declared (say with typedecl) inside the locale context.
Local type parameters are fixed, outside the context they become
arbitrary, and may thus get instantiated.
Now I'm stuck. Can I do what I'm trying to do.? If not, is there a
logical reason why not?
You can define the datatype globally and use it locally. This means its
parameters will be always mentioned (again) in the local situation.
This archive was generated by a fusion of
Pipermail (Mailman edition) and