I know how to use
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?
Did you import
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
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?
This stackoverflow thread might be helpful
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?
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: Dec 07 2023 at 08:19 UTC