Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] typedecl vs. type synonym

Email Gateway (Aug 22 2022 at 15:46):

From: Matthias Perner <perner@cs.tu-darmstadt.de>
Hi,

I currently have two formalizations of the same pen and paper model in
Isabelle. In one of the formalizations type variables are used
extensively to formalize "underspecified sets" from the pen & paper
model. In the other formalization the "underspecified sets" are
formalized with typedecl.

Now I try to get an idea what the advantages of the two approaches are,
but I cannot find a suitable starting point for this in the Isabelle
documentation. Any hints? A short reply when to use which style would
also be very welcome.

Thanks,
Matthias

Email Gateway (Aug 22 2022 at 15:46):

From: Lars Hupel <hupel@in.tum.de>
Hi Matthias,

that's more of an open question, really.

First, to clarify, "type synonyms" are just syntactic abbreviations.
They don't exist inside the logic and are not useful to abstract over
anything.

"typedecl" are unspecified types. It's impossible to "instantiate" them
later. If you want to assume anything non-trivial on them, you're going
to need "axiomatization". There's no tooling in Isabelle that will make
you prove that your assumptions are consistent. However, type
declarations can be polymorphic; i.e., it is possible to declare a
polymorphic type and axiomatize polymorphic constants.

However, if you fix a type variable in a locale or some other context,
it is monomorphic. This point is rather subtle. For example, you can't
abstract over the "map" function of functors in HOL, because it would
require a variable type constructor. On the other hand, the advantage is
that you can in fact instantiate locales later on and can give a proof
that the assumptions are consistent.

For locales in particular, see the tutorial:
<https://isabelle.in.tum.de/dist/Isabelle2016-1/doc/locales.pdf>.

Hope that helps.

Cheers
Lars

Email Gateway (Aug 22 2022 at 15:46):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Matthias,

Here's my experience on this. The choice basically depends on what you want to use your
formalisation for. If it's just about a stand-alone formalisation that does not involve
code generation and is not supposed to be re-used by others, then typedecl can make your
life a bit easier, for two reasons:

1. You do not have to drag all those type variables around, i.e., your types get smaller
   and easier to read. In particular, Isabelle has a bad habit of normalising the names of
   type variables. So even if you define your function f with meaningful type variable names,

f :: 'string => 'number => 'output

type inference will just use 'a, 'b, 'c, etc. in your theorem statements (and accordingly
in the error messages when type checking fails).

2. Type constructors declared with typedecl can be polymorphic. That is, you can have
   families of unspecified sets indexed by types. With type variables, you need one type
   variable for every instance you need.

Conversely, typedecl also has some drawbacks. First, code generation (and value and
quickcheck, too) do not work for typedecl's, except for very special cases with a careful
manual setup of the code generator. Moreover, if you ever want to apply your theorem to a
particular case, in which the sets are not unspecified any more, you cannot do this within
the Isabelle/HOL logic.

Andreas

Last updated: Nov 21 2024 at 12:39 UTC