[isabelle-dev] Sort constraints syntax
makarius at sketis.net
Mon Jul 9 23:52:04 CEST 2012
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
>> (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
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
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
f :: \<forall>'a::S. 'a => 'a
f == %x. x
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.
More information about the isabelle-dev