Email Gateway (Aug 18 2022 at 10:45): Email Gateway (Aug 18 2022 at 10:45):From: Michael Norrish <michael.norrish@nicta.com.au>
It seems that I cannot do the following
instance tyop :: (class1, class2) myclass
<some proof>
instance tyop :: (class3, class4) myclass
<some other proof>
where there is no connection between the various class<n>. This is
despite the fact that the proofs themselves do work.
My reading of the "Order-Sorted Unification" paper suggests to me that
I'm bumping my head against the "unnecessarily strong" co-regularity
condition. Is there any prospect of this being weakened?
Failing that, how might I achieve the desired effect? The myclass
axclass has as one of its axioms that the "size" of its types not be
greater than a particular limit. In the binary type operator (array),
the "size" of the type is the product of the "size" of the first
argument to array, and the "number" of the second.
At the moment, in order to get something like
(word32, "10") array
accepted as an instance of myclass, I first have to invent a class
into which I can put word32 (I call it sz4), and then a class for the
type "10", which I call count10. I can then use the definition of the
"size" calculation and the axioms for sz4 and count10 to prove that
the "size" of
('a::sz4, 'b::count10) array
is 40, which is less than the limit in myclass.
But if I'm interested in also showing
(some_user_type, "13") array
is in myclass, I'm now stuck.
Thanks,
Michael.
Email Gateway (Aug 18 2022 at 10:45):From: Tobias Nipkow <nipkow@in.tum.de>
Michael Norrish schrieb:
Did I write "unnecessarily strong"? Because I don't think it is. If
(during type inference) you unify a type of class myclass with a type
"('a,'b) tyop", in your example it is not clear what the classes of the
subtypes 'a and 'b should be. You have lost the principal types property.
Best
Tobias
Email Gateway (Aug 18 2022 at 10:45):From: Brian Huffman <brianh@cs.pdx.edu>
Hi Michael,
Instead of using the type class mechanism here, you could accomplish what you
want using predicates on types. I'll explain what I mean by this using an
example:
definition
sizelimit :: "nat => 'a itself => bool" where
"sizelimit n (t::'a itself) == ALL x::'a. size x <= n"
Now you can use this predicate to represent sort constraints. For example,
instead of proving "instance word32 :: sz4" you would prove a theorem that
says "sizelimit 4 TYPE(word32)". This is basically what Isabelle's axclass
system does internally (except that it doesn't allow you to parametrize a
class by a natural number, of course).
You could also prove an inference rule like this for tyop:
[| sizelimit m TYPE('a); sizelimit n TYPE('b); m * n <= k|]
==> sizelimit k TYPE(('a,'b)tyop)
This is much more flexible than any instance declaration in Isabelle could be.
But the drawback is that you lose automation: Instead of sort annotations you
will need to add explicit sizelimit assumptions to your theorems, which you
will then have to discharge manually using inference rules like the one
above.
Email Gateway (Aug 18 2022 at 10:45):From: Michael Norrish <Michael.Norrish@nicta.com.au>
Brian Huffman wrote:
Instead of using the type class mechanism here, you could accomplish
what you want using predicates on types. ...
This is much more flexible than any instance declaration in Isabelle
could be. But the drawback is that you lose automation: Instead of
sort annotations you will need to add explicit sizelimit assumptions
to your theorems, which you will then have to discharge manually
using inference rules like the one above.
Yes, this would definitely suffice. But I'm afraid it's not really an
option given what we're doing and where we're up to at the moment. We
are making pretty heavy use of our "memtype" class, which encodes "is
representable in memory", and it would be a pain to lose that
automation. We also don't have the time to go back and re-engineer
everything.
We will get round the problem by showing
instance array :: (oneMB_orless, lt_four_thousand) mem_type
once and for all, and then showing that the examples we're working
with satisfy those constraints. (Declaring an array of 5000 ints
won't be allowed, but we're working with a pretty restricted codebase,
so we can be confident that we're happy with this restriction.)
Michael.
Last updated: May 03 2024 at 04:19 UTC