[isabelle-dev] Type variables without default sort

[Makarius]

On Wed, 29 Jun 2011, Tobias Nipkow wrote:

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

I agree, especially what Brian said, but this is only a prefix of a much 
longer story.  Some years ago, we have been deeper down there and found 
more issues (IIRC myself and Florian, and probably Clemens).

Apart from direct user input there are at least two more layers where 
type-inference takes place (aka "term check" phase):

   (1) Packages that prefer to assemble pre-terms with open constraints
     instead of fully and recheck them.

   (2) Target mechanisms like locales that assemble complex expressions
     over specification segments and let type-inference work out the
     remaining details.

Here any small change in the "top sort", "base sort", "default sort" 
behaviour can produce big surprises (like in the Stalker Zone).

This is why I prefer not to tinker there, but improve general user 
feedback about type-inference.  It will also cover the frequent situations 
that are not directly caused by these boundary cases of sort assignment.


 	Makarius