# Re: [isabelle] typedecl versus explicit type parameters

On Wed, 29 Jul 2009, Andreas Lochbihler wrote:

`The Isabelle tutorial mentions typedecl as a simple way to say that a
``type is actually a parameter to some theory development. In particular,
``explicit type parameters for constants, datatypes etc. do not clutter
``the definitions and proofs.
`

`But what if later on, I want to instantiate such a type to a concrete
``type in some application that uses the theory? Can this be done?
`

`You would have to produce a post-hoc axiomatic specification of the type.
``E.g. by postulating "type_definition rep abs A" and maybe reinitializing
``some declarations in imitation of the 'typedef' package.
`

`A slightly more disciplined way would be to reinterpret the whole theory
``in the manner of the AWE tool from Bremen.
`

`If so, can different theories instantiate the type differently? What
``happens then at a theory merge?
`

With raw axiomatizations you would just get an inconsistent theory.

`Are there other ways to fix type parameters such that I don't have to
``write them everywhere?
`

`A locale context can abstract over simple types, but not type constructors
``(this is a fundamental limitation of the logical framework, which lacks
``true polymorphism). See Isabelle2009/src/HOL/ex/Abstract_NAT.thy for an
``example. We are still working on "localizing" more definitional packages,
``to allow them within such a local context (record, datatype in
``particular).
`

`The "target" mechanism behind this idea is fully generic in terms of
``logical interpretation. So one could even think of wrapping up AWE as a
``local theory target, and then allow users to interpret polymorphic type
``and term constants in a disciplined way.
`
Makarius

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