Email Gateway (Aug 18 2022 at 12:39): Email Gateway (Aug 18 2022 at 12:39):From: Rafal Kolanski <rafalk@cse.unsw.edu.au>
Greetings,
I am working with a situation where I want to state that words with
certain properties on their lengths are members of a type class.
However, there seems to be no way to state that a type constructor (in
this case bit0) takes a type class into two different ones.
So if we have words_of_length_2, we can say that:
instance bit0 :: (words_of_length_4) words_of_length_2
If the length is 4, then we know it's divisible by 4:
instance bit0 :: (words_of_length_2) words_div_4
but also
instance bit0 :: (words_div_2) words_div_4
at this point, we are stuck, as the above line will have problems with
arity.
In general, anything of this form doesn't seem to work:
axclass a
axclass b
axclass c
instance bit0 :: (a) b sorry
instance bit0 :: (c) b oops (* FAIL *)
Looking at the papers didn't really enlighten. Is this a fundamental
limitation on type classes? Is there any way to get around it?
Yours Sincerely,
Rafal Kolanski.
Email Gateway (Aug 18 2022 at 12:39):From: Tobias Nipkow <nipkow@in.tum.de>
This is an inherent limitation which allows to infer unique most general
types. The technical details are explained for example here:
http://www4.informatik.tu-muenchen.de/~nipkow/pubs/lf91.html
Sorry about that.
Tobias
Rafal Kolanski wrote:
Email Gateway (Aug 18 2022 at 12:40):From: Brian Huffman <brianh@cs.pdx.edu>
Hi Rafal,
I can suggest a few workarounds for your type arity conflicts. Here is
your basic example:
axclass a
axclass b
axclass c
instance bit0 :: (a) b sorry
instance bit0 :: (c) b oops (* FAIL *)
If class "a" can be proven to be a subclass of class "c", (or
vice-versa) then the conflict will be avoided. For example, this
sequence of commands will work:
axclass a
axclass b
axclass c
instance a < c sorry
instance bit0 :: (a) b sorry
instance bit0 :: (c) b sorry
In your case, I would expect that you should be able to prove that
words_of_length_2 is a subclass of words_div_2; maybe this will solve
your problem.
If proving a subclass relationship is not possible, then another
workaround is possible by declaring a new class whose axioms are a
disjunction of two other classes. For example:
axclass a
axclass b
axclass c
axclass a_or_c
instance a < a_or_c
instance c < a_or_c
instance bit0 :: (a_or_c) b sorry
instance bit0 :: (a) b sorry
instance bit0 :: (c) b sorry
Hope this helps,
Quoting Rafal Kolanski <rafalk@cse.unsw.edu.au>:
Greetings,
I am working with a situation where I want to state that words with
certain properties on their lengths are members of a type class.
However, there seems to be no way to state that a type constructor (in
this case bit0) takes a type class into two different ones.So if we have words_of_length_2, we can say that:
instance bit0 :: (words_of_length_4) words_of_length_2
If the length is 4, then we know it's divisible by 4:
instance bit0 :: (words_of_length_2) words_div_4
but also
instance bit0 :: (words_div_2) words_div_4
at this point, we are stuck, as the above line will have problems with arity.
In general, anything of this form doesn't seem to work:
axclass a
axclass b
axclass c
instance bit0 :: (a) b sorry
instance bit0 :: (c) b oops (* FAIL *)Looking at the papers didn't really enlighten. Is this a fundamental
limitation on type classes? Is there any way to get around it?Yours Sincerely,
Rafal Kolanski.
Email Gateway (Aug 18 2022 at 12:41):From: Rafal Kolanski <rafalk@cse.unsw.edu.au>
Hi Brian,
Your work-arounds (especially the second one) are very interesting, and
will probably prove useful in the future. I experimented with what you
suggested however, for what I'm doing, Tobias' explanation seems to be
the limit.
What I really want is a type class representing words of length 8, 16 or
32. I would then be able to show that words of this class are "storable"
(another class) in the C sense (byte, short, int). However, once I
declare word_len8 to be storable, I can't do that for word_len16 because
bit0 takes word_len8 to word_len16. Sadly, I don't think there is a way
to get around this nicely.
Thank you very much for the suggestions though! I can feel they will get
me out of trouble at some point in the future :)
Sincerely,
Rafal Kolanski.
Brian Huffman wrote:
Email Gateway (Aug 18 2022 at 12:41):From: Brian Huffman <brianh@cs.pdx.edu>
Quoting Rafal Kolanski <rafalk@cse.unsw.edu.au>:
If I understand you correctly, what you need is a type class like this
one, which includes only types of size 8, 16, or 32:
axclass card_8_16_32 < finite
card_8_16_32: "CARD('a) = 8 | CARD('a) = 16 | CARD('a) = 32"
However, you also want to be able to show that the type (bit0 'a) is
an instance of this class, for appropriate argument types. I.e., you
need to have a class instance of the form
instance bit0 :: (???) card_8_16_32
Now the question is, what is the most general type class you need to
put in place of the question marks? Since bit0 doubles the cardinality
of its argument type, what you need is a type class that includes only
types of size 4, 8, or 16:
axclass card_4_8_16 < finite
card_4_8_16: "CARD('a) = 4 | CARD('a) = 8 | CARD('a) = 16"
Now you can prove the following:
instance bit0 :: (card_4_8_16) card_8_16_32
Of course, now we need to provide another instance to show that bit0
'a :: card_4_8_16 for appropriate argument types. So we just repeat
the process, adding more type classes until we get to class card_1,
which serves as a base case.
axclass card_2_4_8 < finite
card_2_4_8: "CARD('a) = 2 | CARD('a) = 4 | CARD('a) = 8"
axclass card_1_2_4 < finite
card_1_2_4: "CARD('a) = Suc 0 | CARD('a) = 2 | CARD('a) = 4"
axclass card_1_2 < finite
card_1_2: "CARD('a) = Suc 0 | CARD('a) = 2"
axclass card_1 < finite
card_1: "CARD('a) = Suc 0"
instance bit0 :: (card_2_4_8) card_4_8_16
instance bit0 :: (card_1_2_4) card_2_4_8
instance bit0 :: (card_1_2) card_1_2_4
instance bit0 :: (card_1) card_1_2
instance num1 :: card_1_2_4
instance num1 :: card_1_2
instance num1 :: card_1
We can show that these instance declarations are sufficient by
declaring the following constant:
consts
store :: "'a::card_8_16_32 => int list"
term "store (x::32)" (* OK *)
term "store (x::16)" (* OK *)
term "store (x::8)" (* OK *)
term "store (x::64)" (* type error *)
term "store (x::20)" (* type error *)
Hopefully these type classes will work for you. However, I expect that
defining overloaded operations on these type classes might be a bit
tricky. Constant definitions would probably need to do case analysis
on the cardinality of the type argument, but I haven't tried this.
Email Gateway (Aug 18 2022 at 12:41):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Dear Rafal,
I have barely to add anything to Brian's excellent solution proposal
except that you should consider using Isabelle's class / instantiation
instead of the primitive axclass / instance. A short tutorial can be
found at http://isabelle.in.tum.de/dist/Isabelle/doc/classes.pdf.
Perhaps it is sufficent to provide a combinator like
definition bit_length_case :: "'b itself => 'a => 'a => 'a => 'a" where
"bit_length_case TYPE('b) f g h = (if CARD('b) = 16 then f else if
CARD ('b) = 8 then g else ..."
Hope this helps
Florian
signature.asc
Last updated: May 03 2024 at 12:27 UTC