Am 27/02/2013 16:44, schrieb Makarius: > On Wed, 27 Feb 2013, Tobias Nipkow wrote: > >> definition my0 :: nat where "my0 = length []" >> >> into a definition of a constant of type "'a itself ⇒ nat" with an additional >> parameter. Although this is a legal definition, I never understood why this >> is >> done automatically. The user could also write it explicitly if he really >> wanted it that way. Chances are he did not. Is this functionality actually >> used in the distribution? > > We've had a lot of strange crashes in the past, before it was all unified > towards the implicit introduction of TYPE / itself arguments in a few > well-defined spots. > > There might be other conceptual problems luring, but they did not show up in > the > past few years. > > All known incidents were of the category as the present one: someone who is > not > yet conditioned to watch out for excess polymorphism stumbles over it, and > gets > surprised how ond type parameters here suddenly shows up there. But this can > be > avoided by indicating the spots where polymorphism happens in the sources in a > comprehensive way.
You fixed a problem in one place and it bubbles up as a dubious feature in other places where there was no problem (eg the definition command). Nobody needs the implicit introduction of type arguments in those places because it can be done explicitly (and no example of its usage is seems to exist). Yet your recipe for avoiding the reported confusions is to put out some kind of warning because most likely the system did something the user did not want. Which gets overlooked until the user has been "conditioned". I rest my case. Tobias > (This implicitly assumes that users are using the Isabelle document model, not > the TTY loop. If this is up to discussion, it should go on another thread.) > > > Makarius _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
