[isabelle-dev] Sort constraints syntax

[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