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

[Brian Huffman]

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