[isabelle-dev] Type variables without default sort

[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
>>>
>