[isabelle-dev] Sort constraints syntax
Tobias Nipkow
nipkow at in.tum.de
Fri Jul 6 19:01:05 CEST 2012
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
More information about the isabelle-dev
mailing list