[isabelle-dev] Sort constraints syntax

[Tobias Nipkow]

You write

"The notation would have to prevent any misinterpretation as a local context or
binder just for the type in question."

But that is what is intended. If you look at the prototype that I had sent you
separately, you see that "['a::S]T" is just replaced by "T['a::S/'a]" upon
parsing. A good old parse translation. If there is another 'a outside the scope
of this context, it will not be affected. That will typicaly lead to

*** Inconsistent sort constraints for type variable "'a"

Thus the reader cannot be mislead.

It is just a syntactic shorthand, like many others we have.

Tobias

Am 06/07/2012 15:23, schrieb Makarius:
> On Thu, 19 Apr 2012, Tobias Nipkow wrote:
> 
>> Currently, the sort of a type variable in a type is constrained by attaching
>> "::S" to it. Right in the middel of the type, eg "'a::ord => 'a => bool". This
>> can make types less readable. In Haskell this is expressed with a separate
>> context. After some discussion in Munich we propose to support some such
>> context notation, too. The exact syntax is not determined, but something like
>> "[sort context] type". The type above could then be written as "['a::ord] 'a
>> => 'a => bool". In this instance it may not even look like an improvement, but
>> with larger types and constraints in the middle it does help.
>>
>> This would be syntax only and would be translated away with a parse
>> translation. It would improve legibility of theory documents. Of course one
>> could also imagine types being printed like that.
> 
> This thread has become already quite old, but a related topic about
> SORT_CONSTRAINT has shown up recently.
> 
> 
> Generally, the Isabelle "check" phase takes a list of types + terms to be
> processed simultaneously.  Sort constraints that occur here or there are
> distributed uniformly, to get a consistent sort assignment in the end.
> Constraints from the context are also taken into account.
> 
> The canonical example for is
> 
>   <CONTEXT>
>   theorem
>     fixes <TYPES>
>     assumes/shows <TERMS>
> 
> but there are many other applications, such as the usual specification packages:
> 
>   <CONTEXT>
>   function ... <TYPES>
>     where <TERMS>
> 
> 
> Regular specifications (of terms) do not provide any means for explicit type
> arguments, like ML, but unlike Haskell.  Only type constructors allow explicit
> ('a::S1, 'b::S2) tycon, but have some other restrictions instead. So the idea of
> "[sort context] type" taken from Haskell does not quite fit to Isabelle.
> 
> 
> As hinted above, there are basically 3 ways to specify sort constraints in
> Isabelle:
> 
>   (1) Within the type language, presently as 'a::S for actual occurrences
>     of type variables only.
> 
>   (2) Within the term/prop language, analogous to SORT_CONSTRAINT('a::S).
> 
>   (3) Within the context language, say as a reformed version of the
>     'constrains' element, that could work both for term variables and type
>      variables after some rethinking; potentially also 'constraint' and
>      'constrain' commands for the theory and proof language, respectively.
> 
> Further notes:
> 
> For (1) the notation would have to prevent any misinterpretation as a local
> context or binder just for the type in question.  This concept does not exist in
> Isabelle.
> 
> For (2) the existing SORT_CONSTRAINT had a slightly different motivation, but it
> produces a similar effect.  I have chosen that slightly bulky name to get it out
> of the way of anything else, also to prevent any misinterpretation as a
> judgement that 'a::S holds, which is not the case. SORT_CONSTRAINT('a::S) as a
> proposition is logically vacuous.  So it is logically the same within 'assumes'
> and 'shows', but technically only the assumption is stripped fro the result
> right now.
> 
> For (3) one might be able to unify the train of thoughts with the other "default
> types" project that is still stuck somewhere.  Here are some speculative
> applications of it that could in principle be supported:
> 
>   context constrains 'a::S and x::'a
>   begin ... end
> 
> 
>   bundle foo
>   begin
>     constraint 'a :: S
>     constraint x :: 'a
>   end
> 
>   context includes foo
>   begin ... end
> 
> 
>     Makarius