Re: [isabelle] Arity limitations of type classes?



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:
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,

- Brian


Quoting Rafal Kolanski <rafalk at 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.








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