[isabelle-dev] Type variables without default sort

[Tobias Nipkow]

Point taken. Although it makes me wonder if the default sort in HOLCF is 
too specialised.

Tobias

Am 29/06/2011 18:12, schrieb 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
>>