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
 away.

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 years ago.

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.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.