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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
