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

Overloading是Isabelle逻辑的核心功能。它允许您声明一个可以在特定类型上定义的“广泛”类型的常量。用户很少需要手动执行此操作。它是用于实现类型类的基础机制。例如，如果您按如下方式定义类型类：

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

然后，class命令将声明类型empty的常量'a'，随后的实例化仅针对特定类型（例如empty或nat）提供list的definition。

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

我认为

临时超载是一个误导性的名称。据我了解，它源自Haskell（请参阅this paper from Wadler and Blott）。他们在那里使用它来精确描述在Isabelle中被称为“重载”的类型类机制。在Isabelle中，ad-hoc超载的含义完全不同。这个想法是，您可以使用它来定义抽象语法（如monad的do-notation）Isabelle的ML风格简单类型系统无法准确捕获。与重载一样，您将定义一个“ broad”类型的常量。但是该常量永远不会收到任何定义！而是使用更特定的类型定义new常量。当Isabelle的术语解析器遇到抽象常数的使用时，它将尝试用具体常数replace对其进行替换。

例如：您可以对option，list和其他一些类型使用注释符号。如果您编写类似的内容：

do { x <- foo; bar }

然后伊莎贝尔看到：

Monad_Syntax.bind foo (%x. bar)

在第二步中，根据foo的类型，它将把它翻译为以下可能术语的one：

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

同样，用户可能不需要显式处理此概念。如果从库中提取Monad_Syntax，您将可以轻松配置一个临时超载应用程序。

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