[isabelle-dev] Sort constraints syntax

[Makarius]

On Fri, 6 Jul 2012, Tobias Nipkow wrote:

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

You cannot count on that error, it merely indicates that certain 
implementations are still more sequential than they could or should be. 
(E.g. next time I manage to get type-checking for 'theorem ... obtains' 
right, it might also change its behaviour slightly to make it less 
sequential in type-inference.)

Historically, the parser would assign sort constraints only within the 
scope of a single term.  A term without any sort constraints would get all 
type variables decorated with the "default" sort from the context (which 
could stem from earlier constraints in the text).

So there was an accidental preference from left-to-right for terms in the 
specification, and undecorated type variables could get "stuck" with a 
default sort that was assigned too early, and later in conflict with 
constraints given by the user.  (After amending that recently, typedef, 
record, datatype could suddenly take sort constraints for their argument 
types on the LHS as well.)


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

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

Back to this situation, which is the one in your example.  This syntax 
allows to "factor out" sort constraints from certain sub-expressions of 
the type language.  Such "contexts" could be nested, could cover some 
sub-expressions, and others not.  So certain type variables will get 
decorated with sorts, and according to the simultaneous check model, be 
distributed uniformly over the whole problem (list of types + list of 
terms, or w.l.o.g. just list of terms). This means one cannot think of the 
body of the context as a closed scope (which is no problem, until one 
pretends otherwise).

BTW, the syntax should probably also ensure that nesting sort contexts 
excludes seemingly inconsistent constraints, e.g. ['a::S1] (... ['a::S2] 
... T) are rejected if S1 and S2 are not equal in the sense of the syntax 
layer.

These are really just some observation of what the syntax translation 
does, thinking in terms of Isabelle instead of Haskell.  Nothing else.


Jump to Haskell.  Just before getting on a plane for Bremen on Sunday, 
I've convinced myself that the Haskell report from 1998 (which I still 
remember) and the more current one from 2010 agree in the syntax for type 
class constraints.  So it is not part of the language of types, but of 
declarations: e.g. like f :: context => type.

This roughly corresponds to pro-forma bounded quantification of the most 
general type, what is sometimes used to explain some forms of 
polymorphism:

    f :: \<forall>'a::S. 'a => 'a
    f == %x. x

etc.

But this is not how it actually works in Isabelle, whose type-system is 
quite different from that of Haskell.  And the initial "type declaration" 
of the defined terms are just another spot to provide constraints.

In particular, the \<forall>'a::S above would have to move before all 
'fixes' and 'assumes'/'shows' of the specification (the wording of these 
elements may differ). This means the place for an actual \<forall>'a::S 
context fragment in Isabelle would be an Isar context element (cf. 
'constrains' mentioned already).


Summary: possibilities (1) type language and (2) term language mean that 
constraints somehow float freely, and affect other conccerrences 
indirectly, even ones that might visually look "out of scope"; (3) means 
there is an explicit Isar context around the whole specification 
('function', 'definition', 'theorem' etc.) to modify the constraints 
outside the language of types/terms.


 	Makarius