What's the difference between `overloading` and `adhoc_overloading`?

Question

The Isabelle reference manual describes to ways to perform type-based overloading of constants: "Adhoc overloading of constants" in section 11.3, and "Overloaded constant definitions" in section 5.9.

It seems that 5.9 overloading requires all type parameters to be known before it decides on an overloaded constant, whereas 11.3 (adhoc) overloading decides on an overloaded constant if there is only one matching:

consts 
  c1 :: "'t ⇒ 'a set"
  c2 :: "'t ⇒ 'a set"

definition f1 :: ‹'a list ⇒ 'a set› where 
  ‹f1 s ≡ set s›

adhoc_overloading
  c1 f1

overloading
  f2 ≡ ‹c2 :: 'a list ⇒ 'a set›
begin
  definition ‹f2 w ≡ set w›
end

context 
  fixes s :: ‹int list›
begin
  term ‹c1 s› (* c1 s :: int set *)
  term ‹c2 s› (* c2 s :: 'a set  *)
end

What's the difference between the two? When would I use one over the other?

Answer 1

Overloading is a core feature of Isabelle's logic. It allows you to declare a single constant with a "broad" type that can be defined on specific types. There's rarely a need for users to do that manually. It is the underlying mechanism used to implement type classes. For example, if you define a type class as follows:

class empty =
  fixes empty :: 'a
  assumes (* ... *)

Then, the class command will declare the constant empty of type 'a', and subsequent instantiations merely provide a definition of empty for specific types, like nat or list.

Long story short: overloading is – for most purposes – an implementation detail that is managed by higher-level commands. Occasionally, the need for some manual tweaking arises, e.g. when you have to define a type that depends on class constraints.

Ad-hoc overloading is, in my opinion, a misleading name. As far as I understand, it stems from Haskell (see this paper from Wadler and Blott). There, they use it to describe precisely the type class mechanism that in Isabelle would be coined as just "overloading". In Isabelle, ad-hoc overloading means something entirely different. The idea is that you can use it to define abstract syntax (like do-notation for monads) that can't accurately be capture by Isabelle's ML-style simple type system. As in overloading, you'd define a constant with a "broad" type. But that constant never receives any definitions! Instead, you define new constants with more specific types. When Isabelle's term parser encounters the use of the abstract constant, it will try to replace it with a concrete constant.

For example: you can use do-notation with option, list, and a few other types. If you write something like:

do { x <- foo; bar }

Then Isabelle sees:

Monad_Syntax.bind foo (%x. bar)

In a second step, depending on the type of foo, it will translate it to one of these possible terms:

Option.bind foo (%x. bar)
List.bind foo (%x. bar)
(* ... more possibilities ...*)

Again, users probably don't need to deal with this concept explicitly. If you pull in Monad_Syntax from the library, you'll get one application of ad-hoc overloading readily configured.

Long story short: ad-hoc overloading is a mechanism for enabling "fancy" syntax in Isabelle. Newbies may get confused by it because error messages tend to be hard to understand if there's something wrong in the internal translation.