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
locale context.

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.


	Makarius





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