Re: [isabelle] Arity limitations of type classes?

Quoting Rafal Kolanski <rafalk at>:

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.

- Brian

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.