Re: [isabelle] Polymorphism and simple type



On Mon, 17 Jan 2011, Makarius wrote:

You can work schematically wrt. arbitrary types and the system juggles contexts and results in a way that it looks like Hindley-Milner polymorphism.

Moreover see the following paper on local theory specifications:

  Florian Haftmann and Makarius Wenzel. Local theory specifications in
  Isabelle/Isar, In S. Berardi, F. Damiani and U. de Liguoro, editors,
  Types for Proofs and Programs, TYPES 2008. LNCS 5497, Springer, 2009.
  http://www4.in.tum.de/~wenzelm/papers/local-theory.pdf

At the end of section 3 it says:

  Here the type variables 'a need to be fixed in the context, but ?'b is
  arbitrary.  In other words, we have conjured up proper let-polymorphism
  in the abstract syntax layer of Isabelle/Isar, without touching the Pure
  logic. [By extending it towards a more complicated system with
  polymorphism.]

See also the example http://isabelle.in.tum.de/dist/library/HOL/ex/Abstract_NAT.html which defines a "polymorphic" recursion operator on a hypothetical type of natural numbers.


	Makarius





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