“重载”和`adhoc_overloading`有什么区别？

Question

Isabelle参考手册描述了执行基于类型的常量重载的方法:第11.3节中的“临时重载常量”和第5.9节中的“重载常量defi项”。

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

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命令将声明类型为'a'的常量empty，随后的实例化只为特定类型(如nat或list )提供empty的定义。

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

在我看来，-hoc重载是一个误导的名字.据我所知，它起源于Haskell (参见这篇瓦德勒和布洛特的论文)。在那里，他们使用它来精确描述在Isabelle中被创造为“重载”的类型类机制。在伊莎贝尔看来，临时超载意味着完全不同的东西。它的思想是，您可以使用它来定义抽象语法(例如，对monad的do-表示法)，而这些语法不能被Isabelle的ML风格的简单类型系统精确捕获。与重载一样，您将定义一个具有“宽”类型的常量。但这个常数从来没有得到任何定义！相反，您可以定义具有更特定类型的新常量。当Isabelle的术语解析器遇到抽象常量时，它将尝试用一个具体的常量替换它。

例如:您可以对option、list和其他几种类型使用do-表示法。如果你写的东西像：

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，那么就可以很容易地配置一个即席重载应用程序。

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