Yes, it is a problem of unintended generality. The question remains: are
there known situations where it is intended, or could one restrict the
generated type variables in the same way as the explicitly stated ones.
Tobias
Am 29/06/2011 17:23, schrieb Makarius:
On Wed, 29 Jun 2011, Lars Noschinski wrote:
every once in a while, I manage to create a goal state which contains
type variables with the empty sort (for example in f x = 0, x is of
type 'b :: {}, if there are no additional constraints on f. Some
tools don't like this (e.g. metis omits a warning, SMT fails
altogether) and it always takes me a while to find out, what went wrong.
From an user perspective, this behaviour is a bit puzzling, because it
only occurs if a type variable is invented by Isabelle (explicitly
mentioned type variables always get the default sort). So I wonder why
the default sort is not added for invented type variables. Are there
certain situations where type variables with empty sort are needed?
This is an ancient issue, and recurrent source of certain insider jokes.
First of all, this is not the empty sort, but the empty intersection
of type classes i.e. the full sort. Officially it is called the top
sort.
Apart from the default sort, the base sort of the object logic is
also significant. Mixing all that up can lead to very odd situations. I
have occasionally compared this with the Zone of Strugatsky /
Tarkovsky, although the situation has greatly improved internally in the
past few years.
In general I count the surprise for the user of this (correct) behaviour
of type inference as an instance of the general problem of types that
turn out more general than anticipated.
Otherwise some kind of warning (similar to the one emitted if a fresh
type variable is invented for a fix-ed variable) might be useful.
Tobias suggested that such a warning could also be done in a similar
way like for numerals, by adding an ::'a::{} annotation in the output.
This inlined annotation from many years ago was already a slight
improvement over direct warnings on the output channel (which are mostly
ignored by users).
Since output of terms is more and more replaced by immediate source
markup now, one could start thinking of a good visual metaphor for type
inference. So the question is how to present feedback directly in the
place where the user is producing text, not in occasional printout by
the prover in the background.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
