Email Gateway (Aug 19 2022 at 16:00): Email Gateway (Aug 19 2022 at 16:00):From: Gottfried Barrow <igbi@gmx.com>
Hi,
I work with limited knowledge, so if I stumble onto something useful
then I resort to it a lot.
I've resorted a lot to wrapping a type in a datatype to be able to
instantiate the type with type classes.
This question is about "bool list" in particular, but it's also of
interest to me in general.
What I have is "bool list" in a 1-1 relation with non-zero nat, but I
don't use it directly. I put it in a datatype like this:
datatype_new boD = bo_C "bool list"
I did that in the past because:
1) I didn't know how to do what has now come to my mind,
2) but also, I thought that doing such a thing would be hijacking "list".
I have a type class, which I eventually will want to prove some things
about:
class binc =
fixes binc :: "'a => 'a"
This is a binary increment function, which for "bool list" is in this
instantiation, for the moment:
instantiation list :: ("{complete_boolean_algebra, linorder}") binc
begin
primrec binc_list :: "bool list => bool list" where
"binc_list [] = False # []"
|"binc_list (b # bl) = (if b = False then True # bl else False #
(binc_list bl))"
instance ..
end
I got that idea from the increment function in Num.thy.
The part of instantiating "bool list" that was foggy for me was the idea
that I needed to find a bunch of type classes which "bool" satisfies.
The light bulb finally turned on.
For the above, I executed "print_classes" and found that "bool" had been
instantiated for 42 type classes. I picked the two above with the idea
that I need type classes that will give "bool list" enough properites of
"nat" to prove what I need. Those looked like a good start.
Is instantiating "list" like this a bad thing in general?
Thanks,
GB
Email Gateway (Aug 19 2022 at 16:00):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Gottfried,
On 08/09/14 08:00, Gottfried Barrow wrote:
Hi,
I work with limited knowledge, so if I stumble onto something useful then I resort to it a
lot.I've resorted a lot to wrapping a type in a datatype to be able to instantiate the type
with type classes.This question is about "bool list" in particular, but it's also of interest to me in general.
What I have is "bool list" in a 1-1 relation with non-zero nat, but I don't use it
directly. I put it in a datatype like this:datatype_new boD = bo_C "bool list"
I did that in the past because:
1) I didn't know how to do what has now come to my mind,
2) but also, I thought that doing such a thing would be hijacking "list".
I have a type class, which I eventually will want to prove some things about:
class binc =
fixes binc :: "'a => 'a"This is a binary increment function, which for "bool list" is in this instantiation, for
the moment:instantiation list :: ("{complete_boolean_algebra, linorder}") binc
begin
primrec binc_list :: "bool list => bool list" where
"binc_list [] = False # []"
|"binc_list (b # bl) = (if b = False then True # bl else False # (binc_list bl))"
instance ..
end
This will not work the way you expect. To make the list type an instance of binc, you have
to do this for lists of arbitrary elements of the assumed sort
("{complete_boolean_algebra, linorder}" in this example), not for a specific type bool. As
it is now, you define a function binc_list which is completely unrelated to binc. You will
realise this at the latest when you introcude some assumptions about binc and are unable
to prove them for your attempted instantiation.
Note that if you replace False by bot and True by top, then your definition should
generalise to 'a :: {complete_boolean_algebra, linorder}.
Is instantiating "list" like this a bad thing in general?
If you define your own type classes and instantiate them for list, that is all right.
However, you should be very careful when you instantiate list for type classes of HOL/Main
or other people, because this may restrict the interoperability with the formalisations of
others, as type classes may only be instantiated once for each type in one session.
Andreas
Email Gateway (Aug 19 2022 at 16:01):From: Gottfried Barrow <igbi@gmx.com>
On 14-09-08 01:33, Andreas Lochbihler wrote:
This will not work the way you expect. To make the list type an
instance of binc, you have to do this for lists of arbitrary elements
of the assumed sort ("{complete_boolean_algebra, linorder}" in this
example), not for a specific type bool. As it is now, you define a
function binc_list which is completely unrelated to binc. You will
realise this at the latest when you introcude some assumptions about
binc and are unable to prove them for your attempted instantiation.Note that if you replace False by bot and True by top, then your
definition should generalise to 'a :: {complete_boolean_algebra,
linorder}.
Andreas,
Thanks. Abstract thinking, it can incapacitate a majority of neurons. In
this case, among other reasons, because my goal wasn't to generalize
anything for "list".
The syntax 'instantiation list :: ("{......}") binc ' required one or
more type classes between the braces, so I was trying to make it
concrete as possible for "bool", instead of abstract as possible for "'a
list".
So now, using your tip, I've generalized it for "list" with the minimum
requirements:
instantiation list :: ("{bot,top}") binc
begin
primrec binc_list :: "'a list ⇒ 'a list" where
"binc_list [] = bot # []"
|"binc_list (b # bl) = (if b = bot then top # bl else bot # (binc_list bl))"
instance ..
end
I make "binc" a syntactic type class, and I guess in future, if I build
on that with "assumes" in type classes designed for my other concrete
datatypes, I then should try to figure if my assumptions are applicable
to "'a list".
Is instantiating "list" like this a bad thing in general?
If you define your own type classes and instantiate them for list,
that is all right. However, you should be very careful when you
instantiate list for type classes of HOL/Main or other people, because
this may restrict the interoperability with the formalisations of
others, as type classes may only be instantiated once for each type in
one session.
Specifically, I wanted to decide if I could instantiate "list" for
"numeral", to get the convenience of using standard number syntax with
"bool list", since it's 1-to-1 with non-zero nat, but I had the right,
foggy idea to begin with, that I shouldn't be hijacking "list" like that.
So, I think the answer is that I can instantiate "list" for my own
syntactic type classes, but I should rarely, if ever, instantiate a
general HOL type for any general HOL type class.
Thanks,
GB
Last updated: May 06 2024 at 16:21 UTC