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



On 25/05/18 16:51, Dominique Unruh wrote:
> 
> I am not sure the following situation should be considered a bug or not,
> since it occurs only when using Isabelle incorrectly. But I feel that it
> probably indicates that invalid input is not detected in time, and it may
> lead to very hard to understand problems (starting from a typo). So I just
> explain the problem and leave it to the Isabelle-experts to decide whether
> it indicates a real problem or not.

This preface already points in the direction of a "general user error",
or rather a mismatch of expectations vs. the reality of how the system
works.


> The problem is exhibited by the theory below. But in a nutshell, we have
> the following situation:
> 
>    - It is possible to prove a theorem with a type variable called *a* (not
>    *'a*). I understand that I should not do that, of course. But there is
>    no error when proving the theorem.
>    - Then, if we try to use OF with that theorem, we get unexpected
>    failures. But only if *a* is the name of a fixed variable (not type
>    variable).
> 
> I guess that type variable *a* should probably just be rejected when trying
> to prove the theorem. But even if not, it is surprising that the existence
> of a fixed variable *a* makes a difference since I would have assumed that
> free variables and free type variables have completely independent name
> spaces.

There are many different notions of names, variables, contexts etc. and
a lot of system infrastructure to help getting Isabelle/ML tool
implementations right. The "implementation" manual explains some of this
-- beyond that it is important to find good examples and study them
carefully.

In general, the programming interfaces are much less typed than one
might expect. As a start you should think of Isabelle/ML is a variant of
LISP with a few static types to avoid utter nonsense. It is important to
observe certain disciplines and high-level ideas -- the system often
does not check or cannot check for that.

For type and term variables, it is usually already an error if literal
names appear in the ML text. There are operations to invent fresh
variables relative to a certain context -- and using them is mandatory
to make things work in arbitrary contexts. So it is unlikely to make a
typo of "a" vs. "'a" in ML, because both are already wrong as literal
variable names in the source.


> val ctx = @{context}

First note that there are hard and fast naming conventions for certain
basic Isabelle/ML types (see chapter 0 in the "implementation" manual),
in particular the value above needs to be called "ctxt". Otherwise there
is no chance to understand the source in more complex situations, when
there is a serious problem with contexts (the present example is not
serious yet). The Highlighter of Isabelle/jEdit can be helpful here,
when sources are written in a standard form.

> fun tac {context=ctx, ...} = ALLGOALS (simp_tac ctx)

At this spot you are binding the same name "ctx" again: this shadowing
makes it difficult to understand and change the sources later. Anyway,
the forward definition of "tac" is better inlined into the Goal.prove
invocation, it makes the source more readable and robust.

Here is that snippet in standard form, optimized for readability:

ML ‹
val ctxt = @{context}
val T = TFree ("a", @{sort type})
val l = Free ("l", T)
val thm =
  Goal.prove ctxt ["l"] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (l, l)))
    (fn {context = ctxt', ...} => ALLGOALS (simp_tac ctxt'))
›

Now the development of the local ctxt into ctxt' becomes clear: the
latter is the "eigen-context" of the goal statement.


After inspecting contexts, I routinely look at variables and terms vs.
these contexts. Above Goal.prove is applied to some proposition that is
not declared in the context (e.g. with Variable.declare_term). Omitting
that in real applications can lead to really confusing situations with
the implicit Hindley-Milner polymorphism and other corner cases.

See also section "6.1 Variables" in the "implementation" manual,
including its minimal examples. With that you might produce fresh
type/term variables robustly, such that the whole question from the
start disappears.


	Makarius




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