*To*: Brian Huffman <brianh at cs.pdx.edu>*Subject*: Re: [isabelle] Arity limitations of type classes?*From*: Rafal Kolanski <rafalk at cse.unsw.edu.au>*Date*: Sun, 30 Nov 2008 18:11:25 +1100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <20081129161802.xhxt0ml40kwwc88c@webmail.pdx.edu>*References*: <492CD723.9070308@cse.unsw.edu.au> <20081129161802.xhxt0ml40kwwc88c@webmail.pdx.edu>*User-agent*: Thunderbird 2.0.0.18 (X11/20081125)

Hi Brian,

Sincerely, Rafal Kolanski. Brian Huffman wrote:

Hi Rafal,I can suggest a few workarounds for your type arity conflicts. Here isyour 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", (orvice-versa) then the conflict will be avoided. For example, thissequence of commands will work:axclass a axclass b axclass c instance a < c sorry instance bit0 :: (a) b sorry instance bit0 :: (c) b sorryIn your case, I would expect that you should be able to prove thatwords_of_length_2 is a subclass of words_div_2; maybe this will solveyour problem.If proving a subclass relationship is not possible, then anotherworkaround is possible by declaring a new class whose axioms are adisjunction 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_4at this point, we are stuck, as the above line will have problems witharity.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.

**Follow-Ups**:**Re: [isabelle] Arity limitations of type classes?***From:*Brian Huffman

**References**:**[isabelle] Arity limitations of type classes?***From:*Rafal Kolanski

**Re: [isabelle] Arity limitations of type classes?***From:*Brian Huffman

- Previous by Date: Re: [isabelle] Arity limitations of type classes?
- Next by Date: Re: [isabelle] conversion in Isabelle
- Previous by Thread: Re: [isabelle] Arity limitations of type classes?
- Next by Thread: Re: [isabelle] Arity limitations of type classes?
- Cl-isabelle-users November 2008 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list