[isabelle-dev] Sort constraints syntax

[Tobias Nipkow]

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.

Reactions?

Tobias