[isabelle-dev] Type variables without default sort

[Tobias Nipkow]

I see. Makes sense. Yes, a "most general logical sort" would settle the 
issue, but since it is not much of an issue, I don't think we will 
introduce yet another concept. But at least now we know why identifying 
these two default sorts is not a good idea.

Thanks
Tobias

Am 29/06/2011 19:01, schrieb Brian Huffman:
> On Wed, Jun 29, 2011 at 9:19 AM, Tobias Nipkow<nipkow at in.tum.de>  wrote:
>> Point taken. Although it makes me wonder if the default sort in HOLCF is too
>> specialised.
>
> Why? What other sort do you think might be suitable as a default sort for HOLCF?
>
> Currently, the only purpose of the "default_sort" command that I know
> of is to save typing for users, so they don't have to repeat the same
> class annotations over and over. In HOLCF theories, 95% of type
> variables should have sort "domain", so this is the only sensible
> choice for the default sort in HOLCF.
>
> If type inference were to be modified so that every inferred type
> variable was restricted to have the default sort, then the default
> sort for HOLCF would be forced all the way up to class "type", since
> that class is used occasionally in HOLCF theories. A less-bad choice
> would be to not use the *default sort*, but maintain a separate "most
> general logical sort" that could be used for this purpose. HOLCF could
> set the default sort to "domain", but leave the most general logical
> sort set to "type".
>
> However, I think a better approach to avoiding unwanted top-sort type
> variables is to put an implicit sort constraint on every lambda
> binder, since (as far as I know) this is the only situation that
> causes the problem. I think you would want something with an effect
> similar to the following abbreviation:
>
> abbreviation (input)
>    Lambda :: "('a::type ⇒ 'b::type) ⇒ 'a ⇒ 'b" (binder "Λ " 10)
>    where "Lambda f ≡ f"
>
> term "λ x. True" (* 'a::{} ⇒ bool *)
> term "Λ x. True" (* 'a::type ⇒ bool *)
>
> - Brian
>
>>
>> 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
>>>>
>>