Isabelle中`overloading`与`adhoc_overloading`的区别及适用场景咨询

Great question! Let’s unpack the two type-based constant overloading methods in Isabelle, using your provided code as a concrete reference to clarify their differences and ideal use cases.

Key Differences Between the Two Overloading Approaches #

1. Type Resolution Logic & Binding Behavior #

• Adhoc Overloading (adhoc_overloading): This mechanism resolves the overloaded constant as soon as there’s a unique type match in the context. It scans existing constants bound to the overloaded name and selects the only one that fits the inferred type. In your example, when you write c1 s where s is an int list, Isabelle immediately recognizes that f1 (bound to c1) has the type 'a list ⇒ 'a set, which matches perfectly. So it resolves c1 s to f1 s with the concrete type int set. If multiple constants bound to c1 fit the context, Isabelle will throw an ambiguity error.
• Overloaded Constant Definitions (overloading block): This method requires all type parameters to be fully specified before resolving to a concrete instance. It prioritizes preserving polymorphism until every type variable is pinned down. In your example, c2 s shows up as 'a set because even though s is an int list, the 'a type variable hasn’t been explicitly fixed. Only when you add a type annotation like c2 s :: int set will Isabelle bind it to the f2 definition.

2. Definition Workflow #

• Adhoc Overloading: It’s a "retroactive binding" approach. You first define your concrete constants (like f1), then use adhoc_overloading to map them to a shared overloaded name (like c1). This is great for reusing existing functions under a single, intuitive name.
• Overloaded Constant Definitions: It’s a "proactive declaration" approach. You first declare the link between the overloaded name (c2) and the specific instance type ('a list ⇒ 'a set), then define the instance function (f2) inside a local block. This lets you create dedicated instances for the overloaded name without relying on pre-existing functions.

3. Polymorphism Preservation #

• Adhoc Overloading: Once the context provides enough type information to pick a unique instance, the overloaded name loses its polymorphism in that context—it’s treated as the concrete function it resolved to.
• Overloaded Constant Definitions: The overloaded name retains its polymorphic nature by default. It only resolves to a concrete instance when every type variable is explicitly constrained, making it easier to work with generic code that needs to stay flexible until later.

Ideal Use Cases for Each Approach #

When to Use Adhoc Overloading #

• You want to unify multiple existing functions under a single name (e.g., overloading size to work on lists, sets, and trees).
• You need the overloaded constant to resolve automatically in contexts where the type is unambiguous. This is common for operator overloading (like + for integers, reals, and polynomials) where the context clearly dictates which implementation to use.
• You prefer a lightweight way to reuse existing definitions without wrapping them in additional blocks.

When to Use Overloaded Constant Definitions #

• You need to preserve polymorphism for the overloaded name until all type parameters are explicitly set. This is useful for generic libraries where you want functions to stay flexible during type inference.
• You’re creating custom, dedicated instances for an overloaded name rather than reusing existing functions. The local begin-end block keeps the instance definition encapsulated and tied directly to the overloaded constant’s type signature.
• You want to avoid ambiguity errors in contexts where multiple instances might fit—by requiring full type specification, you force explicit clarity instead of relying on Isabelle to guess.

内容的提问来源于stack exchange，提问作者Søren Debois