Email Gateway (Aug 19 2022 at 08:35): Email Gateway (Aug 19 2022 at 08:35):From: "Aaron W. Hsu" <arcfide@sacrideo.us>
Dear Isabelle Users:
I was wondering what the best, most convenient way to deal with
numbers would be. Specifically, I have a datatype that I want
to be something like 'a mytype, where 'a should usually be either
an int or a nat or some other sort of number. Inside this type
will be a list of 'a list. I then want to have another function
that has the type of "'a mytype => 'a list" that will generate
lists containing all zeros. I am not really sure what the best
way to do this is, because Isabelle complains to me about the 0
not matching the type, since Isabelle doesn't know that I only
want 'a to be numbers. Is there some good way to do this"
Yours truly,
Aaron W. Hsu
Email Gateway (Aug 19 2022 at 08:44):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Dear Aaron,
Isabelle has a mechanism called "type classes" (or "sorts") to restrict the range of a type variable like 'a. "0" is defined in the "zero" type class, "1" in "one", and arbitrary numerals in "numeral". For example:
datatype 'a mytype = MyType "'a list"
fun only_zeros :: "'a mytype => ('b::zero) list" where
"only_zeros (MyType ns) = map (%x. (0::'b::zero)) ns"
value "only_zeros (MyType [1, 2, 3])"
Notice the syntax: "::" attaches a type class constraint to a type variable in a similar way that it attaches a type to a term; in fact, in "0::'b::zero", both uses of "::" are present.
If you need both zeros and ones, you can use "'b::{zero,one}". See the Isabelle tutorial, section 8.3, for details:
http://isabelle.in.tum.de/dist/Isabelle2012/doc/tutorial.pdf
Regards,
Jasmin
Last updated: Nov 21 2024 at 12:39 UTC