Re: [isabelle] Isar polymorphism problem
On Mon, 28 Apr 2014, Peter Lammich wrote:
You can prove the statement
\<exists>f::'a1 => ... => 'an => 'b. P f
However, in the proof you cannot make any additional assumptions about
the type variables, in particular you cannot instantiate them.
The only way in Isabelle/HOL to express types with certain properties
are type-classes, which have several restrictions, e.g., they can only
depend on one type variable.
This sounds a bit too much like a magic addition of type classes to
Isabelle, but that is not the case. It is also not directly related to
My TPHOLs paper from 1997 about type classes in Isabelle explains how that
slightly extended type system fits nicely into the existing logical
framework of Isabelle/Pure (which is a minimal version of H.O.L.).
As a spin-off you can also work with so-called "hidden polymorphism"
(which is related to "phantom types" elsewhere) using the type constructor
'a itself and the notation TYPE('a) in Pure. A predicate with more than
one TYPE('a) argument represents a general relation of types.
Doing that without the high-level interfaces of Isabelle type classes is
an arcance discipline, though. And the type-inference for type classes
does depend on the single-argument restriction, to keep things simple.
This archive was generated by a fusion of
Pipermail (Mailman edition) and