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.

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

See also the example which defines a "polymorphic" recursion operator on a hypothetical type of natural numbers.


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