[isabelle-dev] Fwd: A possible bug with Isabelle 2013

[Tobias Nipkow]

Am 27/02/2013 15:28, schrieb Makarius:
> On Wed, 27 Feb 2013, Lawrence Paulson wrote:
> 
>> A behaviour where "..." denotes something other than the previous right-hand
>> side needs to be fixed.
> 
> Again this odd "bug -- fixed" terminology. Such problems are much deeper.
> 
> Fortunately, the solution for overly polymorphic results, and the extreme form
> of so-called hidden-polymorphism, has been mostly there for several years.  We
> had really big structural problems in the past, but this is now forgotten.

The solution you allude turns the definition

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?

Tobias

> What is missing is some immediate visual feedback about what the system has
> produced from user input.  This applies to plain Hindley-Milner generalization,
> implicit itself arguments, and coercions.
> 
> Note that in mainstream programming communities, even just Hindley-Milner
> without anything in addition is often found in the "type-inference sucks" corner
> of discussion forums.
> 
> 
>     Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev