Wolfgang Jeltsch (May 11 2023 at 15:57): Wolfgang Jeltsch (May 11 2023 at 15:57):I know how to use consts and overloading, but I have some trouble understanding adhoc_overloading, whose documentation in the Isabelle/Isar Reference Manual is quite terse. What makes matters worse is that I can’t even conduct experiments with adhoc_overloading, as Isabelle/HOL seems to not treat adhoc_overloading as a keyword. Can someone please enlighten me regarding how adhoc_overloading is to be used and whether it is even supported in Isabelle/HOL?
Lukas Stevens (May 11 2023 at 20:07):Did you import HOL-Library.Adhoc_Overloading?
Wolfgang Jeltsch (May 11 2023 at 20:20):You have to import something? I think that wasn’t mentioned in the Isabelle/Isar Reference Manual. I’m actually surprised, since adhoc_overloading seems more basic to me than overloading.
How does adhoc_overloading actually relate to overloading? To me it seems that it creates the same kind of overloadings of constants declared with consts and the difference is that adhoc_overloading uses existing constants as concrete versions of the abstract constants while overloading asks you to locally introduce new constants to be used as concrete versions of the abstract constants. Is this correct and the whole story, or have I misunderstood or missed something?
Simon Roßkopf (May 11 2023 at 20:30):This stackoverflow thread might be helpful
Wolfgang Jeltsch (May 15 2023 at 12:13):Thanks a lot for this link.
My use case is common notation for different tuples of types (something I could solve with multi-parameter type classes in Haskell). So far, I thought that overloading would generally be the way to go, as it is more high-level, but this StackOverflow thread suggests that adhoc_overloading is to be used in such situations.
What are the pros and cons of the two mechanisms? I understand that with overloading you don’t get this exponentially growing number of different parse trees out of which hopefully only one is type-correct, which is an issue when using the same notation for entirely different constants or abbreviations. Will I reintroduce this problem when switching to adhoc_overloading, because ad-hoc overloading is resolved by the term parser?
Wolfgang Jeltsch (May 15 2023 at 13:07):I experimented a bit with adhoc_overloading, which improved my intuition about it.
One thing I found, which was not surprising given the explanation in this StackOverflow thread, was that with adhoc_overloading you cannot introduce generic definitions on top of your overloaded constants, since apparently they have to be resolved immediately.
For example, assume you have a constant (+) and a few implementations of it using ad-hoc overloading. Then you want to define summing the elements of a list using (+) for any type that has a (+) implementation, but you can’t: Isabelle wants to use a particular (+) implementation also in your definition of list summing.
In my use case, I want to have a generic definition, however. The above-mentioned StackOverflow thread presents adhoc_overloading as a means to define shared syntax. My use case is mostly about defining shared syntax too, but I think that adhoc_overloading isn’t really helpful here, because I want to have that generic definition in addition. In fact, my use case seems to be much more like a use case for type classes, and the only reason why I’m resorting to bare overloading at all is that Isabelle doesn’t support multi-parameter type classes. Using overloading gets reasonably close to multi-parameter type classes though, which is probably why using it seems to be the correct choice in my situation.
Last updated: May 01 2024 at 20:18 UTC