Re: [isabelle] Arity limitations of type classes?
Quoting Rafal Kolanski <rafalk at cse.unsw.edu.au>:
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.
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:
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and