Re: [isabelle] typedecl vs. type synonym
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.
On 11/07/17 10:30, Matthias Perner wrote:
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and