Re: [isabelle] typedecl vs. type synonym

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.


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 MHonArc.