On Wed, Dec 1, 2010 at 11:50 PM, Tobias Nipkow <[email protected]> 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 _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
