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
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
* 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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and