*To*: Rafal Kolanski <rafalk at cse.unsw.edu.au>*Subject*: Re: [isabelle] Arity limitations of type classes?*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Wed, 26 Nov 2008 11:43:35 +0100*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <492CD723.9070308@cse.unsw.edu.au>*References*: <492CD723.9070308@cse.unsw.edu.au>*User-agent*: Thunderbird 1.5.0.7 (X11/20060909)

http://www4.informatik.tu-muenchen.de/~nipkow/pubs/lf91.html Sorry about that. Tobias Rafal Kolanski wrote:

Greetings,I am working with a situation where I want to state that words withcertain properties on their lengths are members of a type class.However, there seems to be no way to state that a type constructor (inthis 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 fundamentallimitation on type classes? Is there any way to get around it?Yours Sincerely, Rafal Kolanski.

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

- Previous by Date: [isabelle] about longer computation syntax sugar
- Next by Date: Re: [isabelle] about longer computation syntax sugar
- Previous by Thread: [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