Email Gateway (Aug 19 2022 at 17:05): Email Gateway (Aug 19 2022 at 17:05):From: Andrew Gacek <andrew.gacek@gmail.com>
I have a class defined as
class foo =
fixes foo :: 'a
and I am trying to instantiate it over the type "string" but I get an error:
instantiation "string" :: foo
Bad type name: "String.string"
Knowing that string is "char list" I tried that instead, but still got an error:
instantiation "char list" :: foo
Undefined type name: "char list"
Is there any way to instantiate the class over the type "string" like I want?
I know I could try to instantiate at "char" and then do something
general for "list", but it turns out the definitions I want for the
type "char list" are not the same as doing this for char and then
lifting it to lists.
Perhaps I have to wrap "string" in a datatype to get what I want?
Thanks,
Andrew
Email Gateway (Aug 19 2022 at 17:06):From: Tobias Nipkow <nipkow@in.tum.de>
I'm afraid Isabelle's type classes are the classical Haskell ones, no
extensions. Either do it for lists in general or wrap string in a datatype. Or
use a locale instead of a class.
Tobias
smime.p7s
Email Gateway (Aug 19 2022 at 17:06):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Andrew,
You can instantiate a type class only for a type constructor such as "list", not for
compound types such as "char list". Since "string" is a type synonym of "char list", the
type class instantiation for "string" must match the instantiation for "char list". If
"char list" and "string" must have different instantiations, then you have to use some
other type constructor that is isomorphic to string, and do the instantiation for it.
Note that the type "String.literal" from theory String is such a copy, but I recommend
that you do not use this type copy for your purposes. String.literal has a specific
purpose for code generation, so if you ever want to generate code (especially in Haskell),
you will run into problems with String.literal.
Hope this helps,
Andreas
Email Gateway (Aug 19 2022 at 17:06):From: Andrew Gacek <andrew.gacek@gmail.com>
Let me step back and say that what I primarily want is a way to define
a function at multiple different types so that I can use it with the
same syntax in each case. Originally I did this just by using the same
syntactic abbreviation for all of them, but the number of ambiguous
parses grows way too much.
I want something like
swap :: string => string => 'a => 'a
which I will define at various types like string, exp, equation, exp
list, string list, string => nat, etc. It would also be nice if the
cases for exp list and string list were derived from a general pattern
for list.
I've tried using locales just now, but I don't think it provides what
I'm looking for (or perhaps I'm using them wrong). If that's right,
then it seems the only solution would be to wrap types like string and
string => nat into datatypes so that I can instantiate a type class in
an ad-hoc fashion for them. The downside is that having something like
string => nat wrapped in a datatype makes the it more cumbersome to
use since I can no longer just apply it to a string to get back a nat.
Is this an accurate assessment?
Thanks,
Andrew
Email Gateway (Aug 19 2022 at 17:06):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Andrew,
There are two ways that approximate what you want.
consts swap :: "string ⇒ string ⇒ 'a ⇒ 'a"
overloading swap_string ≡ "swap :: string ⇒ string ⇒ char list ⇒ char list" begin
definition "swap_string = (undefined :: string ⇒ string ⇒ char list ⇒ char list)"
end
consts swap :: "string ⇒ string ⇒ 'a ⇒ 'a"
definition swap_string :: "string ⇒ string ⇒ string ⇒ string"
where "swap_string = undefined"
adhoc_overloading swap swap_string
class swap_list
definition swap_list :: "string ⇒ string ⇒ 'a :: swap_list list ⇒ 'a list"
where "swap_list = undefined"
adhoc_overloading swap swap_list
instance int :: swap_list ..
lemma "swap = (swap_list :: _ ⇒ _ ⇒ int list ⇒ _)" ..
lemma "swap = swap_string" ..
You have to instantiate the type class swap_list for all types that you want to use the
generic implementation from list. Since the type of the function swap_list is restricted
to lists over a type that inhabits the class swap_list, type inference will use
swap_string for "char list" (= "string") and swap_list for other types such as "int list".
You cannot use this trick with such a marker type class in the first approach because you
could later on instantiate char and thus create inconcistencies. Since the kernel of
Isabelle only sees the replaced constants swap_list, swap_string, etc., soundness is not a
problem.
Hope this helps,
Andreas
Email Gateway (Aug 19 2022 at 17:07):From: Viorel Preoteasa <viorel.preoteasa@aalto.fi>
Hi Andrew,
Why don't you do it like this:
class foo =
fixes foo :: 'a
instantiation "list" :: (type) foo
begin
instance proof qed
end
You create the instantiation for every kind of lists.
The problem is that instead of char you have an
arbitrary type. If you use some operations on
chars, then this is too abstract, but if you only
work with operations on lists, then this should be
enough.
If you need operations on char in the instantiation,
then you can create another class
class my_char =
fixes "operations on char that you need to abstract"
assumes "properties of the operation on char that you need in the list
:: (type) foo instantiation"
Then you create an instantiation of char as my_char:
class my_char =
fixes my_op :: 'a
class foo_str =
fixes foo_str :: "'a ⇒ 'a"
assumes foo_rule: "foo_str x = foo_str y"
instantiation "char" :: my_char
begin
definition "my_op = CHR ''a''"
instance proof qed
end
instantiation "list" :: (my_char) foo_str
begin
definition foo_my_char_def: "foo_str x = [my_op]"
instance proof qed (simp add: foo_my_char_def)
end
lemma "foo_str (x::string) = foo_str y"
by (rule foo_rule)
This gives you the full power as you would get if
it would be possible to instantiate string as foo.
The drawback is that you need to duplicate in
my_char the operations on characters. You can
do it easily by assuming a bijective function between
my_char and char.
I needed something similar. In my case I needed
to instantiate (nat => 'a::SomeClass) as SomeClass, but it
was not possible, so I created a class Nat, and
I instantiated nat as Nat, and I created the
instance ('a::Nat => 'b::SomeClass) of SomeClass.
You can see the details of this in the archive of formal proofs:
http://afp.sourceforge.net/entries/RefinementReactive.shtml
in the file Temporal.thy
Best regards,
Viorel
Email Gateway (Aug 19 2022 at 17:07):From: Andrew Gacek <andrew.gacek@gmail.com>
Thanks for the suggestion. In the end, I wrapped my strings (and other
types) in a datatype. I added some abbreviations and new syntactic
notation which makes this not as bad as I expected. Plus it now feels
like I'm working with Isabelle rather than against it :-)
-Andrew
Last updated: Apr 26 2024 at 01:06 UTC