[isabelle-dev] Additional type variable(s) in specification

[Tobias Nipkow]

The interface is a red herring. The discussion is on the concept at the
user level. If it is not generally useful but only in very arcane
situations, it should not happen implicitly, but the arcane situations
should be required to state the dependence explicitly. We have this
explicit over implicit principle in many places. A warning that in
essence says "This is most likely not what you wanted, but I'll do it
anyway" is just very odd, no matter how prominently it is displayed.

Surely it would not be that difficult to check whether the implicit
parameterisation has taken place and reject it on the top level, or have
a vesion of the underlying function that does not do the parametrisation
in the first place?

Tobias

Makarius schrieb:
> On Thu, 2 Dec 2010, Tobias Nipkow wrote:
> 
>> Florian explained to me that for the function package this new
>> behaviour is an improvement, but that does not mean that unsuspecting
>> users should be subjected to it.
> 
> Maybe Florian (and Alex) can post again the concrete examples they were
> mentioning to me 1 or 2 years ago.
> 
> As usual with the locale and locale theory specification business, the
> situation is a bit more complex than most people think.  The version of
> 09e238561460 is one more step towards *less* surprise in this
> notoriously difficult issue of hidden polymorphism.  The same technique
> of itself abstractions is used in several other parts of the system, too.
> 
> Right now there is already a clear warning -- which Proof General
> happens to show in a hardly visible way, but that is just one of many
> problems of Proof General.  In Isabelle/jEdit the warning is hard to
> miss. I will check again about the other related messages to increase
> the pontential further.
> 
> 
>     Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev