isabelle - `overloading` 和 `adhoc_overloading` 有什么区别？

Question

Isabelle 引用手册描述了执行基于类型的常量重载的方法:第 11.3 节中的“常量的临时重载”和第 5.9 节中的“重载常量定义”。

似乎 5.9 重载要求在决定重载常量之前知道所有类型参数，而 11.3(即席)重载如果只有一个匹配项，则决定重载常量:

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

两者有什么区别？我什么时候会使用一个？

Answer 1

重载 是伊莎贝尔逻辑的核心特征。它允许您使用可以在特定类型上定义的“广泛”类型声明单个常量。用户很少需要手动执行此操作。它是用于实现类型类的底层机制。例如，如果您定义一个类型类如下:

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

然后， class命令将声明常量 empty类型 'a' ，随后的实例化仅提供 empty 的定义对于特定类型，例如 nat或 list .

长话短说:在大多数情况下，重载是由更高级别命令管理的实现细节。有时，需要进行一些手动调整，例如当您必须定义依赖于类约束的类型时。

临时重载 在我看来，这是一个误导性的名字。据我所知，它源于 Haskell(见 this paper from Wadler and Blott)。在那里，他们使用它来精确描述在 Isabelle 中被称为“重载”的类型类机制。在 Isabelle 中，临时重载意味着完全不同的东西。这个想法是，您可以使用它来定义无法被 Isabelle 的 ML 风格的简单类型系统准确捕获的抽象语法(如 monad 的 do-notation)。与重载一样，您将定义一个具有“广泛”类型的常量。但是这个常量永远不会收到任何定义!相反，您可以使用更具体的类型定义新常量。当 Isabelle 的术语解析器遇到抽象常量的使用时，它会尝试用具体常量替换它。

例如:您可以将 do-notation 与 option 一起使用, list ，以及其他一些类型。如果你写这样的东西:

do { x <- foo; bar }

然后伊莎贝尔看到:

Monad_Syntax.bind foo (%x. bar)

第二步，取决于 foo的类型，它会将其转换为以下可能的术语之一:

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

同样，用户可能不需要明确处理这个概念。如果你拉进来 Monad_Syntax从库中，您将获得一个易于配置的即席重载应用程序。

长话短说:即席重载是一种在 Isabelle 中启用“花哨”语法的机制。新手可能会对此感到困惑，因为如果内部翻译有问题，错误消息往往难以理解。