Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Mysteries of locales, "TYPE(T)", and "T itself"

Email Gateway (Sep 17 2022 at 13:46):

From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
(See attached theory file for full context.)

I have a need to impose constraints on a type, as in the following locale declaration:

locale nondegenerate =
fixes dummy :: 'a
assumes is_nondegenerate: "∃x :: 'a. x ≠ undefined"

This works, and produces in the output window:

locale nondegenerate
fixes dummy :: "'a"
assumes "nondegenerate TYPE('a)"

I then make an interpretation of this locale (output shown as quotations):

context
begin

interpretation nondegenerate ‹undefined :: bool›

proof (prove)
goal (1 subgoal):
1. nondegenerate TYPE(bool)

proof
obtain f :: "bool ⇒ bool" where f: "inj f"
using inj_on_id2 by blast
show "∃x :: bool. x ≠ undefined"
by blast
qed

So far, so good. Then I try:

lemma bool_is_nondegenerate:
shows "nondegenerate (undefined :: bool)"

Type unification failed: Clash of types "bool" and "_ itself"

Type error in application: incompatible operand type

Operator: nondegenerate :: ??'a itself ⇒ bool
Operand: undefined :: bool

Hmm... I try instead:

lemma bool_is_nondegenerate:
shows "nondegenerate (undefined :: bool itself)"
using nondegenerate_axioms
apply blast

theorem bool_is_nondegenerate:
nondegenerate undefined
Failed to apply initial proof method⌂:
using this:
nondegenerate TYPE(bool)
goal (1 subgoal):
1. nondegenerate undefined

In this case, Ctrl-hover in the output window over the
"undefined" in the goal shows "constant: HOL.undefined".

oops

Now I try:

lemma bool_is_nondegenerate:
shows "nondegenerate TYPE(bool)"
..

theorem bool_is_nondegenerate:
nondegenerate TYPE(bool)

This appears to succeed. I now check that this fact allows me to
reinstantiate the locale:

end

context
begin

interpretation nondegenerate ‹undefined :: bool›
using bool_is_nondegenerate by blast

end

This succeeds, so it seems that I have achieved what I wanted. But I don't have
the slightest understanding of the failed cases, nor do I have a very clear idea of
what "TYPE(T)" and "T itself" really are. I have looked on multiple occasions for
some kind of documentation of these constructs, but I could not find any.

Can someone explain how to understand the above? Thanks.

- Gene Stark
Foo.thy

Email Gateway (Sep 20 2022 at 17:26):

From: Manuel Eberl <manuel@pruvisto.org>
Hello,

this mostly isn't really a locale issue, but an issue with the ML-style
ad-hoc polymorphism in Isabelle. This is described briefly in §2.3.2 of
the Isabelle implementation manual. But let me try to explain it here as
well:

Explicit polymorphism would be to model polymorphic constants as
functions that take "type parameters". Isabelle, on the other hand, does
not have explicit type parameters but has a kind of implicit polymorphism.

Consider for instance the following definition:

definition "foo = (∀x. x = x)"

This constant "foo" is of Boolean type, but it is polymorphic – even
though its type itself is not polymorphic. The question of whether "foo"
is true or not depends on the type of the "x" that we are quantifying
over. Of course, this is just not possible. If you have something of
type "bool", it cannot be True in one context and False in another.

The solution to this is hinted at when you look at the warning message
emitted by Isabelle:

Additional type variable(s) in specification of "foo": 'a
and inspecting the actual type of foo:
"foo"
  :: "'a itself ⇒ bool"
Isabelle adds an additional dummy parameter to the "foo" to make this
implicit dependence on the "type parameter" 'a explicit. The type "'a
itself" is essentially a singleton type that only contains the dummy
value "Pure.type :: 'a itself", which can, for convenience, be written
with the syntax "TYPE('a)". Similar tricks are often employed in Haskell
to bring type parameters to the term level.

In practice, these issues rarely show up. One example is something like
the characteristic of a (semi-)ring, where the ring in question comes
from a typeclass. The following is a slightly modified example taken
from the "GCD" theory in the HOL session in the Isabelle distribution:

definition semiring_char :: "'a :: semiring_1 itself ⇒ nat"
  where "semiring_char _ = Gcd {n. of_nat n = (0 :: 'a)}"
Here, the dependence on the type parameter 'a was already made explicit
by adding a dummy "itself" parameter. One could also have done without it:

definition semiring_char :: "nat"
  where "semiring_char = Gcd {n. of_nat n = (0 :: 'a :: semiring_1)}"
In this case, we get the same warning as above and Isabelle would add
the "itself" parameter and the end result would be the same.

In your example, the perhaps confusing bit is that Isabelle seems to
have eliminated your "dummy" parameter (presumably because nothing in
your locale actually depends on the value of "dummy") and then, through
the above mechanism, introduced its own dummy parameter of type "'a
itself". The exact mechanism of elimination of this unnecessary
parameter is not clear to me, especially because it doesn't do this in
other cases, such as "locale foo = fixes x :: bool". There we can do
"interpretation foo True" without an error.

In any case, I would recommend just replacing your "dummy :: 'a"
parameter with a "dummy :: 'a itself" parameter and doing the
interpretation with "TYPE('a)" instead of "undefined :: 'a".

By the way, your "degenerate" locale might as well be turned into a
"degenerate" type class (you do get a "additional type variables"
warning, but you can just ignore it):

class nondegenerate =
  assumes is_nondegenerate: "∃x :: 'a. x ≠ undefined"

instance bool :: nondegenerate
  by intro_classes blast
I for one would however phrase the axiom as "∃x y. x ≠ y" instead.
Logically equivalent, of course, but I for one think it's nicer.

Hope that helps.

Cheers,

Manuel

For the nitpicks: "'a itself" is only a singleton type in the sense that
we cannot prove it to have more than one value. The only way to
construct values of type "'a itself" is through "Pure.type" and of
course things like "undefined" and "SOME x. True". There is no way to
prove that it is a singleton type.

On 17/09/2022 15:46, Eugene W. Stark wrote:

(See attached theory file for full context.)

I have a need to impose constraints on a type, as in the following
locale declaration:

locale nondegenerate =
  fixes dummy :: 'a
  assumes is_nondegenerate: "∃x :: 'a. x ≠ undefined"

This works, and produces in the output window:

locale nondegenerate
  fixes dummy :: "'a"
  assumes "nondegenerate TYPE('a)"

I then make an interpretation of this locale (output shown as
quotations):

context
  begin

interpretation nondegenerate ‹undefined :: bool›

proof (prove)
  goal (1 subgoal):
   1. nondegenerate TYPE(bool)

proof
      obtain f :: "bool ⇒ bool" where f: "inj f"
        using inj_on_id2 by blast
      show "∃x :: bool. x ≠ undefined"
        by blast
    qed

So far, so good.  Then I try:

lemma bool_is_nondegenerate:
    shows "nondegenerate (undefined :: bool)"

Type unification failed: Clash of types "bool" and "_ itself"

Type error in application: incompatible operand type

Operator:  nondegenerate :: ??'a itself ⇒ bool
  Operand:   undefined :: bool

Hmm... I try instead:

lemma bool_is_nondegenerate:
    shows "nondegenerate (undefined :: bool itself)"
      using nondegenerate_axioms
      apply blast

theorem bool_is_nondegenerate:
   nondegenerate undefined   Failed to apply initial proof method⌂:
  using this:
    nondegenerate TYPE(bool)
  goal (1 subgoal):
   1. nondegenerate undefined

In this case, Ctrl-hover in the output window over the
"undefined" in the goal shows "constant: HOL.undefined".

oops

Now I try:

lemma bool_is_nondegenerate:
    shows "nondegenerate TYPE(bool)"
      ..

theorem bool_is_nondegenerate:
   nondegenerate TYPE(bool)

This appears to succeed.  I now check that this fact allows me to
reinstantiate the locale:

end

context
  begin

interpretation nondegenerate ‹undefined :: bool›
      using bool_is_nondegenerate by blast

end

This succeeds, so it seems that I have achieved what I wanted. But I
don't have
the slightest understanding of the failed cases, nor do I have a very
clear idea of
what "TYPE(T)" and "T itself" really are.  I have looked on multiple
occasions for
some kind of documentation of these constructs, but I could not find any.

Can someone explain how to understand the above?  Thanks.

- Gene Stark

Email Gateway (Sep 21 2022 at 10:39):

From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
On 9/20/22 13:26, Manuel Eberl wrote:

Hello,

this mostly isn't really a locale issue, but an issue with the ML-style ad-hoc polymorphism in Isabelle. This is
described briefly in §2.3.2 of the Isabelle implementation manual. But let me try to explain it here as well:

Thanks for this pointer. For some reason, "TYPE" and "itself" did not make it into to the index of
this document. I am pondering what it says in §2.3.2. As is my usual experience with the core Isabelle documentation,
I feel as though one has to understand everything before understanding anything, but it is a start.

Explicit polymorphism would be to model polymorphic constants as functions that take "type parameters". Isabelle, on the
other hand, does not have explicit type parameters but has a kind of implicit polymorphism.

Consider for instance the following definition:

definition "foo = (∀x. x = x)"

This constant "foo" is of Boolean type, but it is polymorphic – even though its type itself is not polymorphic. The
question of whether "foo" is true or not depends on the type of the "x" that we are quantifying over. Of course, this is
just not possible. If you have something of type "bool", it cannot be True in one context and False in another.

The solution to this is hinted at when you look at the warning message emitted by Isabelle:

Additional type variable(s) in specification of "foo": 'a
and inspecting the actual type of foo:
"foo"
  :: "'a itself ⇒ bool"
Isabelle adds an additional dummy parameter to the "foo" to make this implicit dependence on the "type parameter" 'a
explicit. The type "'a itself" is essentially a singleton type that only contains the dummy value "Pure.type :: 'a
itself", which can, for convenience, be written with the syntax "TYPE('a)". Similar tricks are often employed in Haskell
to bring type parameters to the term level.

Very helpful, thank you.

In practice, these issues rarely show up. One example is something like the characteristic of a (semi-)ring, where the
ring in question comes from a typeclass. The following is a slightly modified example taken from the "GCD" theory in the
HOL session in the Isabelle distribution:

definition semiring_char :: "'a :: semiring_1 itself ⇒ nat"
  where "semiring_char _ = Gcd {n. of_nat n = (0 :: 'a)}"
Here, the dependence on the type parameter 'a was already made explicit by adding a dummy "itself" parameter. One could
also have done without it:

definition semiring_char :: "nat"
  where "semiring_char = Gcd {n. of_nat n = (0 :: 'a :: semiring_1)}"
In this case, we get the same warning as above and Isabelle would add the "itself" parameter and the end result would be
the same.

In your example, the perhaps confusing bit is that Isabelle seems to have eliminated your "dummy" parameter (presumably
because nothing in your locale actually depends on the value of "dummy") and then, through the above mechanism,
introduced its own dummy parameter of type "'a itself". The exact mechanism of elimination of this unnecessary parameter
is not clear to me, especially because it doesn't do this in other cases, such as "locale foo = fixes x :: bool". There
we can do "interpretation foo True" without an error.

One reason for the explicit "dummy" parameter is that I have a collection of related locales that need to ensure
that the same type is referred to in each of them. If the parameter is included, then the types are forced to be
the same via the fact that the same parameter "dummy" is taken by all the locales. If the parameter is
omitted, then a fresh type variable is introduced during type inference and this connection is not obtained.

In any case, I would recommend just replacing your "dummy :: 'a" parameter with a "dummy :: 'a itself" parameter and
doing the interpretation with "TYPE('a)" instead of "undefined :: 'a".

I will think about this and try it -- thanks.

By the way, your "degenerate" locale might as well be turned into a "degenerate" type class (you do get a "additional
type variables" warning, but you can just ignore it):

class nondegenerate =
  assumes is_nondegenerate: "∃x :: 'a. x ≠ undefined"

instance bool :: nondegenerate
  by intro_classes blast

I will also think about this.

I for one would however phrase the axiom as "∃x y. x ≠ y" instead. Logically equivalent, of course, but I for one think
it's nicer.

Hope that helps.

Yes, thank you very much for taking the time to respond. -- Gene Stark

Cheers,

Manuel

For the nitpicks: "'a itself" is only a singleton type in the sense that we cannot prove it to have more than one value.
The only way to construct values of type "'a itself" is through "Pure.type" and of course things like "undefined" and
"SOME x. True". There is no way to prove that it is a singleton type.

On 17/09/2022 15:46, Eugene W. Stark wrote:

(See attached theory file for full context.)

I have a need to impose constraints on a type, as in the following locale declaration:

locale nondegenerate =
  fixes dummy :: 'a
  assumes is_nondegenerate: "∃x :: 'a. x ≠ undefined"

This works, and produces in the output window:

locale nondegenerate
  fixes dummy :: "'a"
  assumes "nondegenerate TYPE('a)"

I then make an interpretation of this locale (output shown as quotations):

context
  begin

interpretation nondegenerate ‹undefined :: bool›

proof (prove)
  goal (1 subgoal):
   1. nondegenerate TYPE(bool)

proof
      obtain f :: "bool ⇒ bool" where f: "inj f"
        using inj_on_id2 by blast
      show "∃x :: bool. x ≠ undefined"
        by blast
    qed

So far, so good.  Then I try:

lemma bool_is_nondegenerate:
    shows "nondegenerate (undefined :: bool)"

Type unification failed: Clash of types "bool" and "_ itself"

Type error in application: incompatible operand type

Operator:  nondegenerate :: ??'a itself ⇒ bool
  Operand:   undefined :: bool

Hmm... I try instead:

lemma bool_is_nondegenerate:
    shows "nondegenerate (undefined :: bool itself)"
      using nondegenerate_axioms
      apply blast

theorem bool_is_nondegenerate:
   nondegenerate undefined   Failed to apply initial proof method⌂:
  using this:
    nondegenerate TYPE(bool)
  goal (1 subgoal):
   1. nondegenerate undefined

In this case, Ctrl-hover in the output window over the
"undefined" in the goal shows "constant: HOL.undefined".

oops

Now I try:

lemma bool_is_nondegenerate:
    shows "nondegenerate TYPE(bool)"
      ..

theorem bool_is_nondegenerate:
   nondegenerate TYPE(bool)

This appears to succeed.  I now check that this fact allows me to
reinstantiate the locale:

end

context
  begin

interpretation nondegenerate ‹undefined :: bool›
      using bool_is_nondegenerate by blast

end

This succeeds, so it seems that I have achieved what I wanted. But I don't have
the slightest understanding of the failed cases, nor do I have a very clear idea of
what "TYPE(T)" and "T itself" really are.  I have looked on multiple occasions for
some kind of documentation of these constructs, but I could not find any.

Can someone explain how to understand the above?  Thanks.

- Gene Stark

Email Gateway (Sep 22 2022 at 15:12):

From: Andreas Lochbihler <mail@andreas-lochbihler.de>
Dear Eugene,

One more addition to Manuel's excellent explanation: A locale
declaration defines a constant with the same name as the locale that
collects all the assumptions of the locale in a predicate. As arguments,
the constant takes those locale parameters that actually appear in the
assumptions. In your locale, the dummy parameter does not show up in the
locale assumptions. Accordinglz, the generated constant nondegenerate is
defined as

"nondegenerate == ∃x :: 'a. x ≠ undefined"

This definition depends on the type variable 'a very much similar to
Manuel's foo. Therefore, Isabelle's definition facilities add the "'a
itself" parameter to make this dependence explicit.

I'd recommend to avoid this roundabout way of introducing a type
dependency by adding a vacuous assumption involving dummy, for example

locale nondegenerate = fixes dummy :: 'a
assumes is_nondegenerate: "∃x :: 'a. x ≠ undefined"
and dummy: "dummy = dummy"

This will make the constant nondegenerate depend on the parameter dummy,
so its type is now "'a => bool" and there's no hidden polymorphism any
more. You can of course change dummy's type to "'a itself" to make
explicit that the locale does not care about the particular value chosen.

The benefit of adding the dummy assumption can be seen when you have
multiple such parameters in a locale:

locale l = fixes dummy1 :: "'a itself" and dummy2 :: "'b itself"
assumes "∃x :: 'b. x ≠ undefined" "∃x :: 'a. x ≠ undefined"

Here, the order of the itself arguments to the generated constant l
depends on the Isabelle internals for making the hidden polymorphism
explicit. In particular, they are not controlled by the order of the
locale arguments. This is brittle and possibly confusing. Instead, if
you explicitly add the vacuous assumptions, you're in control of the
order of parameters.

Best,
Andreas

Email Gateway (Sep 22 2022 at 21:47):

From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
Thank you, Andreas, your note is also very helpful.

Though I can't say my understanding is crystal clear just yet, I've been able to rework things
using what Manuel and you have said and arrive at something less obscure and redundant and
in general more to my taste.

I have taken into consideration your "dummy = dummy" suggestion, but I am currently not liking
it so much, due to the extra trivial proof obligations that are introduced when the locales are
interpreted. But I might change my mind if I run into the brittleness that you indicate.

-- Gene Stark

Last updated: Apr 20 2024 at 08:16 UTC