# 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.*