Re: [isabelle] Variables in locale assumptions
On Tue, 25 Feb 2014, Andreas Lochbihler wrote:
On 24/02/14 23:05, Makarius wrote:
The 'constrains' element is easier to get rid of. I would like to see
some constructive proofs where you "need to constrain types", as you
say. This is usually just a workaround to specify locale type
arguments, but if that would be supported directly, the need would go
I know one use case where constrains is more convenient than parameter
instantiation with for, namely to revert the renaming of type variables.
I want type variables to have sensible names like 'state, not just 'a,
'b, 'c, 'd. Unfortunately, locale inheritance always renames them to 'a,
'b, 'c, etc., so I rename them back.
This is an old misunderstanding: there is no "locale inheritance", but
locale import within a certain language of locale expressions. That works
via Hindley-Milner type-inference, so the result typing is most-general
and in canonical form. Whence the (fortunate) renaming. Type-inference
was not there in very early versions of locales, which made them hardly
usable, and that was indeed unfortunate.
Of course, this can be done with a for clause, too. But a for clause
drops the mixfix syntax associated with the parameter, so would have to
redeclare it; with constrains, I need not. And for consistency reasons,
I prefer not to redeclare notation if it's not necessary. And if locale
inheritance did not rename type variables, I'd not need constrains at
all and be much happier.
Nothing of this is new in the argument, we've had that already several
What you merely need here is some way to specified the implicit type
arguments of a locale explicitly. That would also help in situations of
"hidden polymorphism", i.e. locales with excess type parameters that are
not mentioned in any term parameter. The existing implementation is a bit
weak here: it emits a warning and leaves the user confused, hoping that
nothing bad happens later.
These fine-points could have been sorted out many years ago, if there
would not be this "lock-in" effect of early aspects of an implementation
that get stuck because users get used to them.
This archive was generated by a fusion of
Pipermail (Mailman edition) and