[isabelle-dev] Type variables without default sort

[Tobias Nipkow]

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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev