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

[Tobias Nipkow]

Thank you Brian, that seems to sum up the situation rather nicely. We
should return to the old behaviour at the top level where definitions
did not acquire additional parameters. 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.

Tobias

Brian Huffman schrieb:
> On Wed, Dec 1, 2010 at 11:50 PM, Tobias Nipkow <nipkow at in.tum.de> wrote:
>> Is the following behaviour really a good idea and useful?
>>
>> inductive P :: "nat => bool" where
>> "P(suc n)"
>>
>> is accepted but defines
>>
>> P :: "'a itself => nat => bool"
>>
>> It does kind of warn me by saying
>>
>> ### Additional type variable(s) in specification of P: 'a
>>
>> but if you miss that warning, you will be very surprised about the kind
>> of errors you get later on when using P.
>>
>> If I give a constant an explicit type, I would prefer Isabelle to
>> respect that.
>>
>> Tobias
> 
> This "feature" seems to originate here:
> http://isabelle.in.tum.de/repos/isabelle/rev/09e238561460
> 
> Another complaint about this behavior appeared recently on the users
> mailing list:
> https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2010-November/msg00065.html
> 
> I agree that the least confusing/surprising behavior would be to have
> definitions like this (taken from the NEWS file) produce an error
> message:
> 
> definition unitary :: bool where "unitary = (ALL (x::'a) y. x = y)"
> 
> In the rare case where someone actually wants to have the definition
> depend on a type variable, it is not a burden to write it explicitly:
> 
> definition unitary :: "'a itself => bool" where "unitary (t::'a
> itself) = (ALL (x::'a) y. x = y)"
> 
> (It used to be possible to write TYPE('a) as a lhs pattern in
> definitions, like "unitary TYPE('a) = (ALL (x::'a) y. x = y)". Why
> doesn't this work any more?)
> 
> This also has the benefit of more clearly indicating the user's intentions.
> 
> I can only think of two situations where adding an implicit TYPE
> parameter makes sense:
> 
> 1. When defining locale predicates, when there are assumptions but no
> value parameters.
> 
> locale count = assumes ex_inj: "EX f::'a => nat. inj f"
> 
> The locale predicate "countable" has type "'a itself => bool", which
> makes sense. Currently it is also possible to make this dependence on
> the type variable more explicit (although this looks a bit messy):
> 
> locale count = fixes dummy :: "'a itself" assumes ex_inj: "EX f::'a =>
> nat. inj f"
> 
> But if we had something like a "fixes" clause for types, it would look
> nicer and indicate the intention unambiguously, making a warning
> message unnecessary:
> 
> locale count = fixes_type 'a assumes ex_inj: "EX f::'a => nat. inj f"
> 
> 2. When defining constants inside locales whose right-hand sides
> depend on locally-fixed type variables, the global versions of the
> constants can have extra TYPE parameters.
> 
> locale count = assumes ex_inj: "EX f::'a => nat. inj f"
> begin
> definition unitary1 :: bool where "unitary = (ALL (x::'a) y. x = y)"
> definition unitary2 :: bool where "unitary = (ALL (x::'b) y. x = y)"
> end
> 
> Within the locale, we have "unitary1 :: bool", but outside the locale,
> we have "count.unitary1 :: 'a itself => bool". (unitary2 has type "'b
> itself => bool" inside and outside the locale.) The current locale
> mechanism implements this correctly, although "unitary1" and
> "unitary2" both produce the same warning message. Ideally, I think it
> would be best for "unitary1" to produce no warning at all, but for
> "unitary2" to be rejected with an error.
> 
> Besides these two very specific cases, I think it would be best to
> reject definitions with extra type variables on the right-hand side.
> 
> - Brian