Email Gateway (Feb 22 2023 at 12:19): Email Gateway (Feb 22 2023 at 12:19):From: Christoph Sprenger <sprenger@inf.ethz.ch>
Dear all,
I have run into the following problem with a locale interpretation (thanks to my colleague Joshua Schneider for minimizing a larger example):
locale test = fixes x :: "'a list"
begin
definition is_empty :: bool where "is_empty ⟷ x = []"
end
definition alist :: "'a ⇒ 'a list" where "alist a = [a]"
interpretation atest: test "alist a" for a :: 'a .
term "test.is_empty (alist a)" ― ‹@{typ "bool"}›
term atest.is_empty ― ‹@{typ "'a itself ⇒ 'a ⇒ bool"}›
term "atest.is_empty TYPE('a)" ― ‹@{typ “‘a ⇒ bool”}›
I would expect atest.is_empty to have type “'a ⇒ bool”. Why do we see the additional parameter of type “‘a itself” here? Also, is there a way to obtain the type I am expecting?
I am aware that such additional parameters of type “‘a itself” appear in connection with hidden polymorphism, as for example in
consts f :: "'a ⇒ 'b"
definition g :: "'a ⇒ 'c" where "g = f o f"
term g ― ‹@{typ "'a itself ⇒ 'b ⇒ 'c”}›
but I cannot see any hidden polymorphism in the first example above, as the type variable ‘a actually does occur in the second parameter of atest.is_empty.
Thank you in advance for any help on this!
Best,
Christoph
Email Gateway (Feb 25 2023 at 08:47):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Christoph!
The hidden polymorphism enters the stage in the definition inside the
locale already.
Although the interpretation eliminates the hidden morphism, the shape of
the originating definition determine the shape of definition after
interpretation also.
Hope this helps,
Florian
OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature
Email Gateway (Mar 01 2023 at 20:04):From: Joshua Schneider <dev@jshs.de>
Hi Florian,
I don't understand your explanation.
The constant as defined in the background theory has an explicit
argument of type "'a list", hence there should be no hidden
polymorphism. The interpretation instantiates the argument with a
different one, which still contains the type variable.
My confusion arises because the snippet below does not have or need the
additional 'a itself argument.
context fixes x :: "'a list"
begin
definition is_empty :: bool where "is_empty ⟷ x = []"
end
definition alist :: "'a ⇒ 'a list" where "alist a = [a]"
abbreviation "atest_is_empty a ≡ is_empty (alist a)"
term atest_is_empty
Shouldn't this be equivalent to Christoph's example (ignoring the locale
registration and instantiated definition theorem)?
Cheers,
Joshua
Email Gateway (Aug 09 2023 at 11:34):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Joshua,
I don't understand your explanation.
The hidden polymorphism enters the stage in the definition inside the
locale already.Although the interpretation eliminates the hidden morphism, the shape
of the originating definition determine the shape of definition after
interpretation also.
after reconsidering this thread, here follows an attempt of a more
accurate description.
Logically, there is no hidden polymorphism. The additional TYPE('a)
argument is an artifact of the internal processing of the definition.
I do not know whether this implementation could be amended easily.
My confusion arises because the snippet below does not have or need the
additional 'a itself argument.context fixes x :: "'a list"
begin
definition is_empty :: bool where "is_empty ⟷ x = []"
end
definition alist :: "'a ⇒ 'a list" where "alist a = [a]"
abbreviation "atest_is_empty a ≡ is_empty (alist a)"
term atest_is_emptyShouldn't this be equivalent to Christoph's example (ignoring the locale
registration and instantiated definition theorem)?
The locale registration is indeed the hot spot where the implementation
sophistication comes in. Hence, your example is logically equivalent,
but technically far less involved than Christoph’s.
Cheers,
Florian
OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature
Last updated: Apr 19 2024 at 12:27 UTC