[isabelle-dev] Type variables without default sort

[Brian Huffman]

These kinds of situations come up in HOLCF, which declares a default
sort other than "type". Type variables default to being pointed (class
"pcpo" or "domain") but it is often convenient to be able to infer
unpointed types wherever they may occur (class "cpo" or "predomain").

- Brian

On Wed, Jun 29, 2011 at 8:56 AM, Tobias Nipkow <nipkow at in.tum.de> wrote:
> 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
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>