[isabelle-dev] Sort constraints syntax
makarius at sketis.net
Fri Jul 6 15:23:46 CEST 2012
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
but there are many other applications, such as the usual specification
function ... <TYPES>
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
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.
(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.
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
constraint 'a :: S
constraint x :: 'a
context includes foo
begin ... end
More information about the isabelle-dev