Email Gateway (Aug 18 2022 at 10:49): Email Gateway (Aug 18 2022 at 10:49):From: Nicole Rauch <rauch@informatik.uni-kl.de>
Dear all,
I'm having trouble getting rid of extra type variables that appear on
the right-hand side of a constant definition. This is my setting:
axclass someAxClass < type
consts
a :: "int => ('a::someAxClass)"
b :: "('a::someAxClass) => bool"
Now if I define a constant that groups together these two consts, say
constdefs
c :: "int => bool"
"c x == b (a x)"
I get the error message
*** Specification depends on extra type variables: "'a"
Is there any way to work around this, e.g. can c depend on 'a
(similar to polymorphic datatype declarations) ?
Or is my attempt generally considered bad design and should be
formalized differently?
Thanks for any insights
Nicole Rauch
Email Gateway (Aug 18 2022 at 10:49):From: Tobias Nipkow <nipkow@in.tum.de>
This is a well-known problem with type classes. The point is that your c
might depend on the choice of the intermediate 'a. One way around this
is to annotate "b (a x)" with some specific type.
Tobias
Nicole Rauch wrote:
Email Gateway (Aug 18 2022 at 10:49):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
You can make your definition explicitly dependent on 'a using the
"itself" type:
constsdefs
c :: "'a itself => int => bool"
"c (T::'a itself) (x::'a) == b (a x)"
Hope this helps
Florian
florian.haftmann.vcf
Email Gateway (Aug 18 2022 at 10:49):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Oops, the type annotation was wrong; better try:
constsdefs
c :: "'a itself => int => bool"
"c (T::'a itself) x == b (a x :: 'a)"
Florian
florian.haftmann.vcf
Email Gateway (Aug 18 2022 at 10:49):From: Makarius <makarius@sketis.net>
Just note that there is no need to invent a dummy argument T here, because
the canonical term TYPE('a) of type 'a itself will do the trick.
Makarius
Email Gateway (Aug 18 2022 at 10:52):From: Gerwin Klein <gerwin.klein@nicta.com.au>
Hi Nicole,
*** Type unification failed: No type arity itself :: type
*** Type error in application: Incompatible operand type
[..]
What is wrong here? Is there any way to add extra type variables to the
set specification?
You need to declare somewhere:
arities itself :: (type) type
This probably should be done in HOL.thy in the distribution already, but
currently isn't.
Cheers,
Gerwin
Email Gateway (Aug 18 2022 at 10:57):From: Nicole Rauch <rauch@informatik.uni-kl.de>
Dear all,
many thanks for the input, it has solved my problem! But now I ran
into another problem:
Suppose I have some axiomatic type classes and some constants defined
over them:
axclass A < type
axclass B < type
consts
f :: "'a::A => bool"
g :: "'a::A => 'b::B"
h :: "'b::B => bool"
Now I want to declare a set inductively like this:
consts
x :: "('a::A) set"
inductive x
intros
xf: "f (a::'a::A) ==> a : x"
xg: "h ((g (a::'a::A))::'b::B) ==> a : x"
The second intro rule fails because of an extra type variable.
I tried the same trick as above, declaring the set x like this:
consts
x :: "('a::A * 'b::B itself) set"
inductive x
intros
xf: "f (a::'a::A) ==> (a, TYPE('b::B) ) : x"
xg: "h ((g (a::'a::A))::'b::B) ==> (a, TYPE('b)) : x"
But now, not even the first intro rule is accepted. The error message is
*** Type unification failed: No type arity itself :: type
*** Type error in application: Incompatible operand type
*** Operator: (Pair (a::'a)) :: ??'a => 'a x ??'a
*** Operand: TYPE('b) :: 'b itself
*** The error(s) above occurred for f (a::'a::A) ==> (a, TYPE
('b::B) ) : x
*** At command "inductive".
What is wrong here? Is there any way to add extra type variables to
the set specification?
Thanks a lot in advance
Nicole Rauch
Last updated: May 03 2024 at 08:18 UTC