[isabelle] A parametrised type class for two or more parametrised types?



Dear Isabelle Gurus,

I think I've reached the edge of Isabelle's type system again, but just to be sure of that, I wanted to ask (Brian Huffman rode a white horse to my rescue just recently :). I've tried to make my question as generic as possible.

Let's say I have two parametrised types:
datatype 'a paddr_t = PAddr 'a
datatype 'a vaddr_t = VAddr 'a

which I've made a member of a type class:

class addrs = type
instance paddr_t :: (type) addrs ..
instance vaddr_t :: (type) addrs ..

The issue is having an overloaded addr_val which will pull out the value. Currently I instantiate the types first and so have:
  addr_val :: "'a::addrs => 32 word"
  where (overloaded)
  "addr_val (x::(32 word) paddr_t) == paddr_val x"
  "addr_val (x::(32 word) vaddr_t) == vaddr_val x"

Is there any way to make this generic over the type contained in addresses?
If I just say:
  addr_val :: "'a::addrs => 'b"
then I can define the overloading with:
  "addr_val (x::'b paddr_t) == (paddr_val x)::'b"
  "addr_val (x::'b vaddr_t) == (vaddr_val x)::'b"
but then Isabelle stops helping me whenever I try to use it during specification or simplification, as the return type is just anything. From what I can tell, this isn't possible, even when for any particular type the return type can be inferred.

For nearly all architectures, the 'b will be identical for both definitions. I'm looking for a way to somehow stick it up there with the 'a.

What I want to do is to define a type class which fixes some parameter over multiple types. Intuitively, to go from "'a set" and "'a list" to "'a container", which means something like "'a (set OR list)", so I could define:
  get_a_member :: "('a container) => 'a"
  and then overload it for
  "get_a_member (x::'a list) == ..." and
  "get_a_member (x::'a set) == ..."

I know I could do this with
  datatype 'a container = Set ('a set) | List ('a list)
but I want a conclusive answer whether it can be handled with just the type system.

Could you offer some suggestions?

Yours Sincerely,

Rafal Kolanski.






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