Re: [isabelle] Comparing polymorphic functions
On Thu, Jan 27, 2011 at 11:42 AM, Christian Maeder <Christian.Maeder at dfki.de
> Am 27.01.2011 11:24, schrieb Eg Gloor:
> > Hello
> > With the "=" operator, I can do comparisons like:
> > consts
> > f :: "'a1 => 'a2"
> > g :: "'a1 => 'a2 => 'a3"
> > lemma "f = g"
> > ...
> > But in HOL.thy, it's defined as
> > eq :: "['a, 'a] => bool" (infixl "=" 50)
> > Since Isabelle/HOL is only simply typed with type variables, how come 'a
> > be instantiated to 'a1 => 'a2 and 'b can be instantiated to 'a1 => 'a2 =>
> > 'a3, even they are of different arities?
> type variables of polymorphic functions are implicitly quantified and
> are instantiated with fresh variables for each occurrence in
> applications. Therefore the type of f "'a1 => 'a2" with fresh (aka new)
> variables is unified to say "'b1 => 'b2 => 'b3" of g (with "'a2" being
> specialized to "b2 => 'b3).
Thanks for the reply. So it seems like it isn't simply-typed afterall, since
"'a2" can be specialised to "'b2 => 'b3". Or is that limited to type
variables? If I do something similar with schematic types:
schematic_lemma test: "(x::?'a=>?'b=>?'c) = (y::?'d=>?'e)"
I get a type unification error there. It seems ?'e can't be specialised to
"?'b => ?'c" in this case.
> > However, if f was
> > f :: "real => real"
> > then type unification fails with "f = g".
> > Thx
This archive was generated by a fusion of
Pipermail (Mailman edition) and