Email Gateway (Aug 18 2022 at 12:56): Email Gateway (Aug 18 2022 at 12:56):From: Rafal Kolanski <rafalk@cse.unsw.edu.au>
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.
Email Gateway (Aug 18 2022 at 12:57):From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
Rafal Kolanski wrote:
Dear Isabelle Gurus,
...
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:this looks like the issue of having (type) constructor classes as well
as just type classes, as was introduced into Haskell some time ago.
Sadly Isabelle (and ML, unlike Haskell) has a language of _types_ which
is not higher order (ie, ('a, 'b) tycon, where tycon is not variable, in
contrast to Haskell's tycon a b,
where a and b can be types (of kind TYPE), or type constructors (of kind
TYPE -> TYPE), etc)
Jeremy
Email Gateway (Aug 18 2022 at 12:57):From: Rafal Kolanski <rafalk@cse.unsw.edu.au>
Jeremy Dawson wrote:
Thank you, Jeremy. I had a feeling that I'm at the edge of the type system.
I'm currently getting around the issue by performing the instantiation
in a separate theory which can be swapped to a different one. This sort
of "modularity" though relies heavily on documentation in plain English :)
Sincerely,
Rafal Kolanski.
Last updated: May 03 2024 at 12:27 UTC