Re: [isabelle] Comparing polymorphic functions



On Thu, 3 Feb 2011, Eg Gloor wrote:

If I understand this correctly, schematic variables can be instantiated but schematic *type* variables cannot due to a restriction of type-inference.

Not quite so.  Here is another attempt to summarize the main aspects.

  * Term and type variables can be either "arbitrary" (schematic) or
    "fixed" (non-schematic, free).

  * Schematic term/type variables can be instantiated.  For type variables
    this effectively means some kind of naive polymorphism.

  * Schematic term variables can be explicitly bound via quantification
    (!! / \<And>) with arbitrary nesting; type variables cannot be bound
    like that.

  * Type inference never instantiates schematic term/type variables
    written by the user.

  * Instead, syntactic type-inference parameters get unified during type
    inference, but there is no end-user notation for that (the system
    sometimes prints ??'a).

  * Goal states with schematic type variables are theoretically OK, but
    often break existing proof tools.


Thus, there's no polymorphism of any kind at the meta-level.

The Pure framework indeed lacks proper polymorphism. You only have global types/consts/theorems that can mention arbitrary types ?'a effectivily giving you some outermost quantification here. The rest are conjuring tricks, in the spirit of original Hindley-Milner polymorphism.


Before this is getting more complicated: What is your actual application?


	Makarius





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