Re: [isabelle] Handling of invalid type variable names on ML level



On 25/05/18 21:03, Dominique Unruh wrote:
> 
> Concerning my original confusion: I was wondering how it can be that
> fixing the variable "a" influences the behavior of the (invalid) type
> variable "a". I think the answer is that, while type and regular
> variables are separate, the table that remembers what variables are
> fixed is shared by type and regular variables. Thus fixing the regular
> variable /a/ also fixes the (invalid) type variable /a/. Is that correct?

The aspect of the context that is relevant here is Name.context /
Variable.names_of. That sub-context throws type and term variables into
one pot, and implicitly relies on other policies that ensure that they
are normally not in conflict.

As you can see in the Variable module, there are further intermediate
states of variables, corresponding to declare_names,
declare_constraints, declare_term etc. -- the "implementation" manual
explains some of this.

It is particularly important to develop an intuition how implicitly
declared type variables vs. explicitly fixed term variables give you
Hindley-Milner polymorphism in the end. That is the main purpose of the
whole affair of managing names formally.


> I will try to follow your programming guidelines. But one thing is
> unclear to me in that context: Goal.prove has an argument xs
> (instantiated with ["l"] in my example). I thought I can use xs with a
> hardcoded name because Goal.prove will locally fix that variable. Is
> that incorrect? If it's incorrect, I don't understand how the argument
> xs can be used, because if I get a fresh name via Variable.variant_fixes
> and supply this name in the argument xs, then I get an error that the
> variable is already fixed. So, I see no way how to use the xs argument.

Goal.prove provides a programming interface that corresponds to Isar
"have props if asms for xs", but Goal.prove uses
Variable.add_fixes_direct without any implicit name invention. The names
that you provide need to be "free" in the sense that they can be fixed
in the current context, e.g. because they were invented properly beforehand.

Apart from these explicit term variables, you need to take care about
type variables occurring in the propositions: Variable.declare_term does
that, it ensures that the term is syntactically known to the context.


	Makarius




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