Re: [isabelle] Arity limitations of type classes?

This is an inherent limitation which allows to infer unique most general types. The technical details are explained for example here:

Sorry about that.

Rafal Kolanski wrote:

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.