Re: [isabelle] Comparing polymorphic functions



On Thu, Jan 27, 2011 at 11:42 AM, Christian Maeder <Christian.Maeder at dfki.de
> wrote:

> 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
> can
> > 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.

Eg

HTH Christian
>
> > 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 MHonArc.