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 Isabelle/HOL.

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.


	Makarius




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