Programming Languages Part A Section4 翻译

这里对Section 4进行翻译。

课程主页：

https://www.coursera.org/learn/programming-languages/home

B站搬运：

https://www.bilibili.com/video/BV1dL411j7L7

Coursera编程语言课程 第4节总结

标准说明：本总结涵盖的材料与课堂视频以及随视频发布的材料（幻灯片、代码）大致相同。它有助于以叙述的方式阅读材料，并将整个课程部分的材料放在一份文件中，特别是在以后复习材料时。请在讨论板上报告这些笔记中的错误。

目录

• 什么是类型推断？
• 更全面的ML类型推断实例
• 多态类型的例子
• 可选：值限制
• 可选：一些使类型推断更加困难的事情
• 相互递归
• 用于命名空间管理的模块
• 签名
• 隐藏东西
• 介绍我们的扩展实例
• 我们例子的签名
• 可爱的转折：暴露整个函数
• 签名匹配规则
• 等价的实现
• 不同的模块有不同的类型
• 动机和定义等价
• 无副作用程序设计的另一个特点
• 标准等价
• 重新审视我们对等价的定义

什么是类型推断？

虽然我们已经使用ML类型推断有一段时间了，但我们还没有仔细研究过它。我们将首先仔细了解什么是类型推断，然后通过几个例子看看ML类型推断是如何工作的。

Java、C和ML都是静态类型语言的例子，这意味着每个绑定都有一个”在编译时”确定的类型，也就是说，在程序的任何部分被运行之前。类型检查器是一个编译时程序，它接受或拒绝一个程序。相比之下，Racket、Ruby和Python是动态类型语言，这意味着绑定的类型不会提前确定，例如将42绑定到x，然后将x视为字符串这样的计算会导致运行时错误。在我们用Racket进行一些编程之后，我们将比较静态类型和动态类型的优缺点，作为一个重要的课程主题。

与Java和C不同，ML是隐式类型的，这意味着程序员很少需要写下绑定的类型。这通常是很方便的（尽管有些人不同意它是使代码更容易还是更难读），但决不是改变ML是静态类型的事实。相反，类型检查器必须更加复杂，因为它必须推断（即弄清楚）程序员编写的类型注释“会是”什么。原则上，类型推断和类型检查可以是独立的步骤（推断器可以做它的部分，检查器可以看结果是否应该进行类型检查），但在实践中，它们经常被合并到类型检查器中。请注意，一个正确的类型推断器必须在所有类型存在的情况下找到一个解决方案，否则它必须拒绝该程序。

一种特定的编程语言的类型推断是容易的、困难的还是不可能的，往往不是很明显。它与类型系统的放任程度不成正比。例如，”接受一切”和”不接受任何东西”的”极端”类型系统都是非常容易进行推断的。当我们说类型推断可能是不可能的，我们指的是技术意义上的不可判定性，就像著名的停止问题。我们的意思是存在一些类型系统，对于这些系统，没有一个计算机程序可以实现类型推断，使得

• （1）推断过程总是终止，
• （2）如果推断是可能的，推断过程总是成功的，以及
• （3）如果推断不可能，推断过程总是失败。

幸运的是，ML的设计相当巧妙，所以类型推断可以通过一个相当直接和优雅的算法进行。虽然有些程序的推断过程慢得难以忍受，但人们在实践中编写的程序从来没有引起这种行为。我们将用几个例子来证明ML类型推断算法的关键方面。这将使你感觉到类型推断并不是”魔术”。为了进入其他课程的主题，我们不会描述完整的算法或编写代码来实现它。

ML类型推断最终与参数多态性交织在一起，当推断程序确定一个函数的参数或结果可能是任何东西时，结果类型就会使用'a、'b等。但类型推断和多态性是完全独立的概念：一种语言可以有一个或另一个。例如，Java有泛型，但没有方法参数/结果类型的推断。

ML类型推断概述

这里是ML类型推断工作的概述（更多的例子在后面）：

• 它按顺序确定绑定的类型，使用早期绑定的类型来推断后期绑定的类型。这就是为什么你不能在文件中使用后面的绑定。（当你需要时，使用相互递归，类型推断决定所有相互递归的绑定的类型。相互递归将在本节后面介绍）。
• 对于每个val或fun绑定，它分析绑定以确定关于其类型的必要事实。例如，如果我们看到表达式x+1，我们得出结论，x必须是int类型。我们为函数调用、模式匹配等收集类似的事实。
• 之后，对于函数参数或结果中任何不受约束的类型，使用类型变量（例如'a）。
• （强制值限制——只有变量和值可以具有多态类型，如后所述。）

关于ML类型系统的一个惊人的事实是，这样的”按部就班”从未导致我们拒绝一个可以进行类型检查的程序，我们也从未接受一个我们不应该接受的程序。所以明确的类型注释真的是可选的，除非你使用像#1这样的功能。（#1的问题是，它没有为类型推断提供足够的信息来知道元组/记录应该有哪些其他字段，而ML类型系统需要知道字段的确切数量和所有字段的名称）。

下面是一个初始的、非常简单的例子：

val x = 42
fun f(y,z,w) = if y then z+x else 0

类型推断首先给出了x的int类型，因为42有int类型。接下来我们将通过其他的例子来研究更多的步骤，但在这里让我们只列出关键的事实：

• y必须有bool类型，因为我们在条件中测试它。
• z必须有int类型，因为我们把它加到我们已经确定有int类型的东西上。
• w可以有任何类型，因为它从不被使用。
• f必须返回int，因为它的主体是一个条件，其中两个分支都返回一个int。(如果它们不一致，类型检查就会失败。)

所以f的类型必须是bool * int * 'a -> int。

更详尽的ML类型推断例子

我们现在将逐步完成几个例子，生成类型推断算法需要的所有事实。请注意，人类在做类型推断时，经常会走捷径，就像人类在做算术时一样，但重点是有一个一般的算法，它有条不紊地通过代码收集约束条件，并把它们放在一起以得到答案。

作为第一个例子，考虑推断这个函数的类型：

fun f x =
   let val (y,z) = x in
       (abs y) + z
   end

这里是我们如何推断类型的：

• 看第一行，对于某些类型T1和T2，f必须有T1->T2的类型，在函数体中f有该类型，并且x有T1类型。
• 看一下val-binding，x必须是pair类型（否则模式匹配就没有意义），所以对于某些T3和T4，T1=T3*T4，y有T3类型，z有T4类型。
• 看一下加法表达式，我们从上下文中知道abs的类型是int->int，所以y的类型是T3意味着T3=int。同样地，由于abs y的类型是int，所以+的另一个参数必须是int类型，所以z的类型是T4，意味着T4=int。
• 因为加法表达式的类型是int，所以let表达式的类型是int。因为let表达式的类型是int，所以f的返回类型是int，也就是说，T2=int。

把所有这些约束放在一起，T1=int*int（因为T1=T3*T4），T2=int，所以f的类型是int*int->int。

下一个例子：

fun sum xs =
   case xs of
     [] => 0
   | x::xs' => x + (sum xs')

• 从第一行来看，存在类型T1和T2，使得sum具有类型T1->T2，而xs具有类型T1。
• 从case表达式来看，xs必须有一个与所有模式兼容的类型。看看这些模式，它们都能匹配任何列表，因为它们是由列表构造器构建的（在x::xs'的情况下，子模式匹配任何类型的东西）。因此，由于xs的类型是T1，事实上T1=T3 list（对于某个T3）。
• 看一下case分支的右侧，我们知道它们必须有相同的类型，这个类型就是T2。因为0的类型是int，所以T2=int。
• 再看第二个case分支，我们在x和xs'都可用的情况下对其进行类型检查。由于我们是针对一个T3列表匹配模式x::xs'，所以一定是x有T3类型，xs'有T3 list类型。
• 现在看右边，我们加上了x，所以事实上T3=int。此外，递归调用会进行类型检查，因为xs'有T3 list类型，T3 list=T1，sum有T1->T2类型。最后，由于T2=int，添加sum xs'的类型检查。

把所有东西放在一起，我们得到sum的类型是int list->int。

注意，在我们得到sum xs'之前，我们已经推断出了所有的东西，但我们仍然要检查类型的使用是否一致，否则拒绝。例如，如果我们写了sum x，那就不能进行类型检查，因为它与之前的事实不一致。让我们更透彻地看一下，看看会发生什么：

fun broken_sum xs =
   case xs of
     [] => 0
   | x::xs' => x + (broken_sum x)

• broken_sum的类型推断过程与sum的推断过程基本相同。前面例子中的前四条都适用，给出broken_sum的类型T3 list ->int，x3的类型T3 list，x的类型T3，和xs的类型T3 list。此外，T3=int。
• 我们在调用broken_sum x时偏离了正确的sum的实现。对于这个调用的类型检查，x的类型必须与broken_sum的参数相同，或者说，T1=T3。然而，我们知道T1=T3 list，所以这个新约束T1=T3实际上产生了一个矛盾：T3=T3 list。如果我们想更具体一点，我们可以利用我们的知识，即T3=int，将其改写为int=int list。看一下broken_sum的定义，应该很明显，这正是问题所在：我们试图将x作为int和int list来使用。

当你的ML程序没有通过类型检查时，类型检查器会报告它发现矛盾的表达式以及该矛盾涉及的类型。虽然有时这些信息是有帮助的，但其他时候，实际问题是在不同的表达式上，但类型检查器直到后来才发现矛盾。

多态类型例子

我们剩下的例子将推断出多态的类型。我们所做的就是遵循上面的程序，但是当我们完成后，我们会有一些函数类型的部分仍然是不受约束的。对于每个”可以是任何东西 “的Ti，我们使用一个类型变量（'a，'b，等等）。

fun length xs =
   case xs of
     [] => 0
   | x::xs' => 1 + (length xs')

类型推断的过程与sum的推断很相似。我们最终确定：

• length的类型是T1->T2。
• xs的类型是T1。
• T1=T3 list（由于模式匹配）
• T2=int，因为0是对length的可能调用结果。
• x有T3类型，xs'有T3类型的列表。
• 递归调用length xs'进行类型检查，因为xs'有T3 list类型，也就是T1，即length的参数类型。而且我们可以添加结果，因为T2=int。

所以我们有所有与sum相同的约束，除了我们没有T3=int。事实上，T3可以是任何东西，length会进行类型检查。所以类型推断认识到，当它全部完成时，它的length类型为T3 list -> int，T3可以是任何东西。所以我们最终得到的类型是'a list -> int，正如预期的那样。同样，规则很简单：对于最终结果中不能被约束的每个Ti，使用一个类型变量。

第二个例子：

fun compose (f,g) = fn x => f (g x) 

• 由于compose的参数必须是pair（从用于其参数的模式来看），compose的类型为T1*T2->T3，f的类型为T1，g的类型为T2。
• 由于compose返回一个函数，T3是某个T4->T5，在该函数的主体中，x的类型是T4。
• 所以g的类型一定是T4->T6，也就是说，T2=T4->T6。
• 而f必须对某个T7具有T6->T7的类型，也就是说，T1=T6->T7。
• 但是f的结果是由compose返回的函数的结果，所以T7=T5，所以T1=T6->T5。

把T1=T6->T5，T2=T4->T6，T3=T4->T5放在一起，我们有(T6->T5)*(T4->T6)->(T4->T5)的compose的类型。没有其他东西来约束T4、T5和T6的类型，所以我们把它们一致地替换掉，最后得到('a->'b)*('c->'a)->('c->'b)，正如预期的那样（最后一组括号是可选的，但这只是语法）。

下面是一个更简单的例子，它也有多个类型变量。

fun f (x,y,z) =
    if true
    then (x,y,z)
    else (y,x,z)

• 第一行要求f有T1*T2*T3->T4的类型，x有T1类型，y有T2类型，z有T3类型。
• 条件表达式的两个分支必须具有相同的类型，这就是函数T4的返回类型。因此，T4=T1*T2*T3，T4=T2*T1*T3。这个约束条件要求T1=T2。

把这些约束放在一起（没有其他约束），f将以类型T1*T1*T3->T1*T1*T3对任何类型T1和T3进行类型检查。因此，用一个类型变量替换每个类型，我们得到'a*'a*'b->'a*'a*'b，这是正确的：x和y必须有相同的类型，但z可以（但不需要）有不同的类型。请注意，类型检查器总是要求条件的两个分支以相同的类型进行类型检查，尽管这里我们知道哪个分支将被评估。

可选：值的限制

正如本节到目前为止所描述的，ML类型系统是不健全的，这意味着它将接受运行时可能有错误类型的值的程序，例如在我们期望的字符串的地方放一个int。这个问题是由多态类型和可变引用的组合造成的，而修复方法是对类型系统的一个特殊限制，称为值限制。

这是一个演示该问题的示例程序：

val r = ref NONE (* 'a option ref *)
val _ = r := SOME "hi" (* instantiate 'a with string *)
val i = 1 + valOf(!r) (* instantiate 'a with int *)

直接使用类型检查/推断的规则会接受这个程序，即使我们不应该——我们最终试图在"hi"上加1。鉴于函数/操作符ref ('a -> 'a ref), := ('a ref * 'a -> unit), ! ('a ref -> 'a)，类型检查没有问题。

为了恢复健全性，我们需要一个更严格的类型系统，不允许这个程序进行类型检查。ML所做的选择是防止第一行有多态的类型。因此，第二行和第三行将不会进行类型检查，因为它们不能用字符串或int来实例化一个'a。一般来说，只有当val-bound中的表达式是一个值或一个变量时，ML才会给val-bound中的变量一个多态的类型。这就是所谓的值限制。在我们的例子中，ref NONE是一个对函数ref的调用。函数调用不是变量或值。所以我们得到了一个警告，r被赋予了一个类型?X1 option ref，其中?X1是一个“冗余类型”而不是一个类型变量。这使得r没有用处，后面的行也没有进行类型检查。这个限制成功地使类型系统健全，这一点并不明显，但事实上它是充分的。

对于上面的r，我们可以使用表达式ref NONE，但是我们必须使用一个类型注解来给r一个非多态的类型，比如int option ref。无论我们选择什么，接下来的两行中的一行将不会进行类型检查。

正如我们之前在研究部分应用时看到的那样，即使因为我们没有使用突变，值限制偶尔也会成为一种负担。我们看到这个绑定成为了值限制的受害者，并且没有被做成多态的：

val pairWithOne = List.map (fn x => (x,1)) 

我们看到了多种变通方法。一个是使用一个函数绑定，尽管没有值限制，但这是不必要的函数包装。这个函数的类型是'a list -> ('a * int) list:

fun pairWithOne xs = List.map (fn x => (x,1)) xs 

有人可能会问，为什么我们不能只对引用（我们需要的地方）执行值限制，而不对列表这样的不可变类型执行值限制。答案是ML类型检查器不能总是知道哪些类型是真正的引用，而哪些不是。在下面的代码中，我们需要在最后一行强制执行值限制，因为'a foo和'a ref是同一类型：

type 'a foo = 'a ref
val f : 'a -> 'a foo = ref
val r = f NONE 

当我们在本节后面研究模块系统时，我们将看到类型检查器并不总是知道类型同义词的表示。所以为了安全起见，它对所有的类型都执行了值限制。

可选：使类型推断更加困难的一些事情

现在我们已经看到了ML类型推断的工作原理，我们可以看到两个有趣的观察：

• 如果ML有子类型（例如，如果每个三元组也可以是一个pair），推断将更加困难，因为我们将不能得出 “T3=T1*T2 “这样的结论，因为等价将是过度的限制。相反，我们需要约束条件，表明T3是一个至少有两个字段的元组。根据不同的细节，这可以做到，但是类型推断更加困难，结果也更难理解。
• 如果ML没有参数化的多态性，推断会更加困难，因为我们必须为length和compose等函数挑选一些类型，而这可能取决于它们的使用方式。

相互递归

我们已经看到了很多递归函数的例子，也看到了很多函数使用其他函数作为辅助函数的例子，但是如果我们需要一个函数f调用g，g调用f呢？这当然是有用的，但是ML的规则，即绑定只能使用早期的绑定，这使得它更加困难——哪个应该先来，f还是g？

事实证明，ML对相互递归有特殊的支持，使用关键字and，并将相互递归的函数放在彼此旁边。同样地，我们也可以有相互递归的数据类型绑定。在展示了这些新的结构后，我们将展示你实际上可以通过使用高阶函数来解决缺乏对相互递归函数支持的问题，这在一般情况下是一个有用的技巧，特别是在ML中，如果你不希望你的相互递归函数彼此相邻。

我们的第一个例子使用相互递归来处理一个int list并返回一个bool。如果列表在1和2之间严格交替，并以2结束，则返回true。当然，有很多方法可以实现这样的函数，但我们的方法很好地为每个”状态”（如”接下来必须有1”或”接下来必须有2”）提供了一个函数。一般来说，计算机科学中的许多问题都可以用这种有限状态机来建模，每个状态对应一个相互递归的函数是实现有限状态机的一种优雅方式。（因为所有函数调用都是尾部调用，所以代码在少量空间中运行，就像有限状态机的实现一样。）

fun match xs =
    let fun s_need_one xs =
            case xs of
                [] => true
              | 1::xs’ => s_need_two xs’
              | _ => false
        and s_need_two xs =
            case xs of
                [] => false
              | 2::xs’ => s_need_one xs’
              | _ => false
    in
        s_need_one xs
end

（代码在模式中使用整数常量，这是一个偶尔方便的ML特性，但对示例来说不是必需的。）

在语法方面，我们通过简单地将除第一个函数外的所有函数的关键字fun替换为and来定义相互递归的函数。类型检查器将同时对所有函数（上例中的两个）进行类型检查，允许它们之间的调用，而不考虑顺序。

下面是第二个（愚蠢的）示例，它还使用了两个相互递归的datatype绑定。类型t1和t2的定义是相互引用的，这是通过使用and代替第二个datatype允许的。这定义了两种新的数据类型，t1和t2。

datatype t1 = Foo of int | Bar of t2
and t2 = Baz of string | Quux of t1

fun no_zeros_or_empty_strings_t1 x =
    case x of
        Foo i => i <> 0
      | Bar y => no_zeros_or_empty_strings_t2 y
and no_zeros_or_empty_strings_t2 x =
    case x of
        Baz s => size s > 0
      | Quux y => no_zeros_or_empty_strings_t1 y

现在假设我们想要实现上面代码中的“无零或空字符串”功能，但出于某种原因，我们不想将函数放在彼此相邻的位置，或者我们使用的语言不支持相互递归的函数。我们可以编写几乎相同的代码，方法是将“后续”函数自身传递给“之前”函数的一个版本，该版本将函数作为参数：

fun no_zeros_or_empty_strings_t1(f,x) =
    case x of
        Foo i => i <> 0
      | Bar y => f y

fun no_zeros_or_empty_string_t2 x =
    case x of
        Baz s => size s > 0
      | Quux y => no_zeros_or_empty_strings_t1(no_zeros_or_empty_string_t2,y)

这是函数的参数可以是另一个函数带来的强大的习语。

名称空间管理模块

我们首先展示如何使用ML模块将绑定分离到不同的名称空间。后面的部分将基于这篇材料，介绍更有趣、更重要的主题，即使用模块隐藏绑定和类型。

为了学习ML、模式匹配和函数式编程的基础知识，我们编写了一些小程序，这些程序只是一系列绑定。对于更大的程序，我们希望用更多的结构来组织代码。在ML中，我们可以使用结构来定义包含绑定集合的模块。在最简单的情况下，你可以编写structure Name = struct bindings end，其中Name是结构的名称（你可以选择任何内容；大小写是一种约定），bindings是任何绑定列表，包含值、函数、异常、数据类型和类型同义词。在结构内部，你可以使用早期的绑定，就像我们“在顶层”（即任何模块之外）所做的那样。在结构外部，你通过使用Name.b来引用Name中的绑定b。我们已经使用这个符号来使用函数，比如List.foldl；现在你知道如何定义自己的结构了。

虽然我们在示例中不会这样做，但你可以将结构嵌套在其他结构中，以创建树状层次结构。但在ML中，模块不是表达式：你不能在函数内部定义它们、将它们存储在元组中、将它们作为参数传递等等。

如果在某个范围内使用来自另一个结构的许多绑定，那么编写SomeLongStructureName.foo多次可能会很不方便。当然，可以使用val绑定来避免这种情况，例如val foo=SomeLongStructureName.foo，但是如果我们使用结构中的许多不同绑定（每个绑定都需要一个新变量），或者在模式中使用结构中的构造函数名，那么这种技术是无效的。因此，ML允许你编写open SomeLongStructureName，它提供了对模块签名中提到的模块中任何绑定的“直接”访问（你只需编写foo）。open的作用域是封闭结构的其余部分（或顶层程序的其余部分）。

open的一个常见用途是为模块本身之外的模块编写简洁的测试代码。open的其他用途通常不受欢迎，因为它可能会引入意外的shadow，尤其是因为不同的模块可能会重用绑定名称。例如，列表模块和树模块可能都有名为map的函数。

签名

到目前为止，结构只提供名称空间管理，这是一种避免程序不同部分中的不同绑定相互隐藏的方法。名称空间管理非常有用，但不是很有趣。更有趣的是给出结构签名，这是模块的类型。它们允许我们提供模块外的代码必须遵守的严格接口。ML有几种不同的语法和语义实现方法；我们只展示了一种为模块写下显式签名的方法。下面是一个签名定义和结构定义的示例，说明结构MyMathLib必须具有签名MATHLIB：

signature MATHLIB =
sig
val fact : int -> int
val half_pi : real
val doubler : int -> int
end

structure MyMathLib :> MATHLIB =
struct
fun fact x =
    if x=0
    then 1
    else x * fact (x - 1)
val half_pi = Math.pi / 2.0
fun doubler y = y + y
end

由于:> MATHLIB，结构MyMathLib只有在它实际提供了MATHLIB签名所声称的一切，并且有正确的类型时，才会进行类型检查。签名还可以包含数据类型、异常和类型绑定。因为我们在编译MyMathLib时会检查签名，所以我们可以在检查任何使用MyMathLib的代码时使用这些信息。换句话说，我们可以在假设签名正确的情况下检查客户端。

隐藏事物

在学习如何使用ML模块向客户端隐藏实现细节之前，让我们记住，将接口与实现分离可能是构建正确、健壮、可重用程序的最重要策略。此外，我们已经可以使用函数以各种方式隐藏实现。例如，这三个函数的参数都是原来的两倍，客户（即调用者）无法判断我们是否将其中一个函数替换为另一个：

fun double1 x = x + x
fun double2 x = x * 2
val y = 2
fun double3 x = x * y

我们用于隐藏实现的另一个特性是在其他函数中本地定义函数。我们可以在知道旧版本不受任何其他代码依赖的情况下，在以后更改、删除或添加本地定义的函数。从工程的角度来看，这是一个关键的关注点分离。我可以改进函数的实现，并且知道我不会破坏任何客户端。相反，客户端所能做的任何事情都不能破坏上述功能的工作方式。

但是，如果你想有两个顶层函数，其他模块中的代码可以使用它们，并让它们都使用相同的隐藏函数，该怎么办？有很多方法可以做到这一点（例如，创建函数记录），但是如果有一些顶级函数对模块来说是“私有”的，那就很方便了。在ML中，没有像其他语言中那样的“private”关键字。相反，你使用的签名只提及较少的内容：签名中没有明确说明的任何内容都不能从外部使用。例如，如果我们将上面的签名更改为：

signature MATHLIB =
sig
val fact : int -> int
val half_pi : real
end

然后客户端代码无法调用MyMathLib.doubler。绑定不在范围内，所以不使用它就会通过类型检查。一般来说，我们的想法是，我们可以随心所欲地实现模块，只有在签名中明确列出的绑定才能被客户端直接调用。

介绍我们的扩展示例

我们剩下的模块系统研究将以一个实现有理数的小模块为例。虽然真正的库会提供更多功能，但我们的库只支持创建分数、相加两个分数以及将分数转换为字符串。我们的库打算：

• （1）防止分母为零，
• （2）保持分数的简化形式（3/2而不是9/6，4而不是4/1）。

虽然负分数是可以的，但从内部来看，库从来没有负分母(−3/2而不是3/−2，3/2而不是−3/−2)。下面的结构实现了所有这些想法，使用了辅助函数reduce，它本身使用gcd来化简分数。

我们的模块维护不变量，如代码顶部附近的注释所示。这些是分数的性质，所有函数都假设为真，并保证为真。如果一个函数违反了不变量，其他函数可能会做错误的事情。例如，gcd函数对于负参数是不正确的，但是因为分母从来都不是负的，所以gcd永远不会用负参数调用：

structure Rational1 =
struct
(* Invariant 1: all denominators > 0
   Invariant 2: rationals kept in reduced form, including that
                a Frac never has a denominator of 1 *)
  datatype rational = Whole of int | Frac of int*int
  exception BadFrac
  
(* gcd and reduce help keep fractions reduced,
   but clients need not know about them *)
(* they _assume_ their inputs are not negative *)
  fun gcd (x,y) =
       if x=y
       then x
       else if x < y
       then gcd(x,y-x)
       else gcd(y,x)

   fun reduce r =
       case r of
           Whole _ => r
         | Frac(x,y) =>
           if x=0
           then Whole 0
           else let val d = gcd(abs x,y) in (* using invariant 1 *)
                    if d=y
                    then Whole(x div d)
                    else Frac(x div d, y div d)
								end

(* when making a frac, we ban zero denominators *)
   fun make_frac (x,y) =
       if y = 0
       then raise BadFrac
       else if y < 0
       then reduce(Frac(~x,~y))
       else reduce(Frac(x,y))
 
(* using math properties, both invariants hold of the result
   assuming they hold of the arguments *)
   fun add (r1,r2) =
       case (r1,r2) of
           (Whole(i),Whole(j))   => Whole(i+j)
         | (Whole(i),Frac(j,k))  => Frac(j+k*i,k)
         | (Frac(j,k),Whole(i))  => Frac(j+k*i,k)
         | (Frac(a,b),Frac(c,d)) => reduce (Frac(a*d + b*c, b*d))

(* given invariant, prints in reduced form *)
   fun toString r =
       case r of
           Whole i => Int.toString i
         | Frac(a,b) => (Int.toString a) ^ "/" ^ (Int.toString b)
         
end

我们的例子的签名

现在，让我们尝试为示例模块提供一个签名，这样客户端可以使用它，但不会违反其不变量。

由于reduce和gcd是我们不希望客户依赖或滥用的帮助函数，一个自然签名如下：

signature RATIONAL_A =
sig
datatype rational = Frac of int * int | Whole of int
exception BadFrac
val make_frac : int * int -> rational
val add : rational * rational -> rational
val toString : rational -> string
end

要使用这个签名来隐藏gcd和reduce，我们只需将上面结构定义的第一行更改为structure Rational1:>RATIONAL_A。

虽然这种方法确保客户端不直接调用gcd或reduce（因为它们在模块外“不存在”），但这还不足以确保正确使用模块中的绑定。模块的“正确”含义取决于模块的规格（而不是ML语言的定义），因此，让我们更具体地了解一下有理数库中所需的一些属性：

• 属性：toString始终以简化形式返回字符串表示形式
• 属性：没有代码进入无限循环
• 属性：没有代码被零除
• 属性：没有分母为0的分数

属性是外部可见的；这是我们向客户承诺的。相比之下，不变量是内部的；它们是有关实现的事实，有助于确保属性。上面的代码维护不变量，并在某些地方依赖它们来确保属性，特别是：

• 如果使用参数调用gcd，它将违反属性≤ 0，但由于我们知道分母大于0，reduce可以毫无顾虑地将分母传递给gcd。
• toString和大多数情况下的add不需要调用reduce，因为它们可以假设自己的参数已经是简化形式。
• add使用了数学的特性，即两个正数的乘积为正数，因此我们知道没有引入非正数分母。

不幸的是，在签名RATIONAL_A下，客户仍然必须被信任，不能破坏属性和内部变量！因为签名公开了数据类型绑定的定义，所以ML类型系统不会阻止客户端直接使用构造函数Frac和Whole，从而绕过我们建立和保存不变量的所有工作。客户可能会做出像Rational.Frac(1,0), Rational.Frac(3,~2), Rational.Frac(9, 6)这样的“糟糕”分数。根据我们的规范，任何一种都可能最终导致gcd或toString行为不当。虽然我们可能只打算让客户使用make_frac、add和toString，但我们的签名允许更多。

一种自然的反应是，通过删除行datatype rational=Frac of int*int | other of int来隐藏数据类型绑定。虽然这是正确的直觉，但结果签名毫无意义，将被拒绝：它反复提到一个已知不存在的rational类型。相反，我们想说的是，有一种类型rational，但是客户除了知道它的存在之外，无法知道该类型是什么。在签名中，我们可以使用抽象类型来实现这一点，如该签名所示：

signature RATIONAL_B =
sig
type rational (* type now abstract *)
exception BadFrac
val make_frac : int * int -> rational
val add : rational * rational -> rational
val toString : rational -> string
end

（当然，我们还必须更改结构定义的第一行，以使用此签名。这总是正确的，因此我们将不再提及它。）

抽象类型的这个新特性，只有在签名中才有意义，正是我们想要的。它允许我们的模块定义对某个类型的操作，而不显示该类型的实现。语法只是给出一个没有定义的类型绑定。模块的实现没有改变；我们只是在改变客户拥有的信息量。

现在，客户如何产生有理数？首先，必须使用make_frac。之后，可以使用make_frac或add产生更多的有理数。没有其他方法，所以多亏了我们写make_frac和add的方式，所有的有理数都将以正分母的简化形式出现。

与RATIONAL_A相比，RATIONAL_B的不同之处是构造器Frac和Whole。因此，客户无法直接创建有理数，也无法在有理数上进行模式匹配。他们不知道如何在内部代表他们。他们甚至不知道rational是作为数据类型实现的。

抽象类型在编程中非常重要。

一个可爱的转折：暴露Whole函数

通过抽象rational类型，我们从客户那里删除了Frac和Whole构造函数。虽然这对于确保客户端不能创建一个没有被化简或分母为非正数的分数至关重要，但只有Frac构造函数有问题。由于允许客户端直接创建整数不会违反我们的规范，我们可以添加一个类似的函数：

fun make_whole x = Whole x

在签名中添加val make_whole : int -> rational。但这是不必要的包装函数；一个较短的实现是：

val make_whole = Whole

当然，客户也无法知道我们使用的是哪种make_whole的实现。但为什么要创建一个和Whole一样的新绑定make_whole？与此相反，我们可以直接将构造函数导出为具有这个签名的函数，而不对我们的结构进行任何改变或添加：

signature RATIONAL_C =
sig
type rational (* type still abstract *)
exception BadFrac
val Whole : int -> rational (* client knows only that Whole is a function *)
val make_frac : int * int -> rational
val add : rational * rational -> rational
val toString : rational -> string
end

这个签名告诉客户有一个与Whole绑定的函数，它接收一个int并产生一个rational。这是正确的：这种绑定是结构中的数据类型绑定所创建的东西之一。所以我们暴露了数据类型绑定所提供的部分内容：rational是一个类型，Whole被绑定到一个函数。我们仍然隐藏了数据类型绑定所提供的其余内容：Frac构造函数以及与Frac和Whole的模式匹配。

签名匹配的规则

到目前为止，我们对一个结构是否”应该进行类型检查”的讨论是相当非正式的。现在让我们列举更精确的规则，说明结构与签名相匹配意味着什么。(这个术语与模式匹配无关。) 如果一个结构不匹配分配给它的签名，那么这个模块就不会进行类型检查。一个结构Name称与BLAH签名相匹配，如果：

• 对于BLAH中的每个val-binding，Name必须有一个与该类型或更一般的类型的绑定（例如，即使签名说它不是，实现也可以是多态的——见下面的例子）。这种绑定可以通过val-绑定、fun-绑定或数据类型绑定来提供。
• 对于BLAH中的每个非抽象类型绑定，Name必须有相同的类型绑定。
• 对于BLAH中的每个抽象类型绑定，Name必须有一些创建该类型的绑定（要么是数据类型绑定或类型同义词）。

请注意，Name可以有任何不在签名中的额外绑定。

等价实现

鉴于我们的性质和不变的签名RATIONAL_B和RATIONAL_C，我们知道客户端不能依赖任何辅助函数或模块中定义的有理数的实际表示。因此，我们可以用具有相同属性的任何等效实现替换该实现：只要模块中对toString绑定的任何调用都产生相同的结果，客户就永远无法判断。这是另一项重要的软件开发任务：以不破坏客户的方式改进/更改库。知道客户端遵守由ML签名强制执行的抽象边界是非常宝贵的。

举个简单的例子，我们可以将gcd定义为reduce内部的一个局部函数，并且知道没有客户端会失败，因为他们不能依赖gcd的存在。更有趣的是，让我们改变结构的一个不变量。我们不要把理性简化。相反，让我们在将有理数转换为字符串之前，先将其缩减。这简化了make_frac和add，同时使toString变得复杂，而toString现在是唯一需要reduce的函数。以下是整个结构，它仍然与签名RATIONAL_A、RATIONAL_B或RATIONAL_C匹配：

structure Rational2 :> RATIONAL_A (* or B or C *) =
struct
  datatype rational = Whole of int | Frac of int*int
  exception BadFrac
  
   fun make_frac (x,y) =
       if y = 0
       then raise BadFrac
       else if y < 0
       then Frac(~x,~y)
       else Frac(x,y)
       
   fun add (r1,r2) =
       case (r1,r2) of
           (Whole(i),Whole(j))   => Whole(i+j)
         | (Whole(i),Frac(j,k))  => Frac(j+k*i,k)
         | (Frac(j,k),Whole(i))  => Frac(j+k*i,k)
         | (Frac(a,b),Frac(c,d)) => Frac(a*d + b*c, b*d)
         
   fun toString r =
       let fun gcd (x,y) =
               if x=y
               then x
               else if x < y
               then gcd(x,y-x)
               else gcd(y,x)
           fun reduce r =
               case r of
                   Whole _ => r
                 | Frac(x,y) =>
                   if x=0
                   then Whole 0
                   else
                       let val d = gcd(abs x,y) in
                           if d=y
                           then Whole(x div d)
                           else Frac(x div d, y div d)
                       end
       in
           case reduce r of
               Whole i   => Int.toString i
             | Frac(a,b) => (Int.toString a) ^ "/" ^ (Int.toString b)
       end 
end

如果我们给Rational1和Rational2的签名是RATIONAL_A，两者都会进行类型检查，但客户端仍然可以区分它们。例如，Rational1.toString(Rational1.Frac(21,3))产生 “21/3”，但Rational2.toString(Rational2.Frac(21,3))产生 “7”。但是如果我们给Rational1和Rational2的签名是RATIONAL_B或RATIONAL_C，那么这些结构对于任何可能的客户端都是等价的。这就是为什么一开始就要使用像RATIONAL_B这样的限制性签名的原因：这样你就可以在以后改变结构而不需要检查所有的客户端。

虽然到目前为止我们的两个结构保持着不同的不变性，但它们确实使用了相同的有理数类型定义。对于签名为RATIONAL_B或RATIONAL_C的结构来说，这并不是必须的；具有这些签名的不同结构可以以不同的方式实现该类型。例如，假设我们意识到，在内部对整数进行特殊编码比它的价值更麻烦。我们可以直接使用int*int并定义这个结构：

structure Rational3 :> RATIONAL_B (* or C *)=
struct
   type rational = int*int
   exception BadFrac
   
   fun make_frac (x,y) =
       if y = 0
       then raise BadFrac
       else if y < 0
       then (~x,~y)
       else (x,y)
       
   fun Whole i = (i,1)
   
   fun add ((a,b),(c,d)) = (a*d + c*b, b*d)
   
   fun toString (x,y) =
       if x=0
       then "0"
       else
           let fun gcd (x,y) =
                   if x=y
                   then x
                   else if x < y
                   then gcd(x,y-x)
                   else gcd(y,x)
               val d = gcd (abs x,y)
               val num = x div d
               val denom = y div d
           in
               Int.toString num ^ (if denom=1
                                   then ""
                                   else "/" ^ (Int.toString denom))
           end
end

(这个结构采用了RATIONAL2的方法，即让toString减少分数，但这个问题在很大程度上与rational的定义是正交的。)

请注意，这个结构提供了RATIONAL_B所要求的一切。函数make_frac很有意思，它接收一个int*int，并返回一个int*int，但是客户不知道实际的返回类型，只知道抽象的rational类型。虽然在签名中给它一个rational的参数类型是匹配的，但这将使该模块毫无用处，因为客户端将无法创建一个有理数类型的值。尽管如此，客户不能向add或toString传递任何int*int；他们必须传递他们知道具有rational类型的东西。就像我们的其他结构一样，这意味着只有make_frac和add才能创建有理数，这也是我们所有的不变性的体现。

我们的结构与RATIONAL_A不匹配，因为它没有把rational作为一种数据类型提供给构造函数Frac和Whole。

我们的结构与签名RATIONAL_C相符，因为我们明确地添加了一个正确类型的函数Whole。没有客户能够将我们的”真实函数”与之前的结构将Whole构造函数作为一个函数的做法区分开来。

fun Whole i = (i,1)与val Whole : int -> rational相匹配的事实很有意思。模块中Whole的类型实际上是多态的：'a -> 'a * int。ML签名匹配允许'a -> 'a * int匹配int -> rational，因为'a -> 'a * int比int -> int * int更一般，以及int -> rational是int -> int * int的一个正确抽象。不太正式地说，Whole在模块内有一个多态类型的事实并不意味着签名必须在模块外给它一个多态类型。 事实上，在使用抽象类型时，它不能这样做，因为Whole不能有'a -> int * int或'a -> rational的类型。

不同的模块定义了不同的类型

虽然我们定义了不同的结构（例如：Rational1、Rational2和Rational3），并具有相同的签名（例如：RATIONAL_B），但这并不意味着不同结构的绑定可以相互使用。例如，Rational1.toString(Rational2.make_frac(2,3))不会通过类型检查，这是一件好事，因为它将打印出一个未还原的分数。它不进行类型检查的原因是，Rational2.rational和Rational1.rational是不同的类型。它们不是由同一个数据类型绑定创建的，尽管它们碰巧看起来是一样的。此外，在模块外我们也不知道它们看起来是一样的。事实上，Rational3.toString(Rational2.make_frac(2,3))确实不需要进行类型检查，因为Rational3.toString期望一个int*int，但是Rational2.make_frac(2,3))返回一个由Rational2.Frac构造函数产生的值。

动机和定义等价

一段代码与另一段代码”等价”的想法是编程和计算机科学的基础。每当你简化一些代码或说”这是做同样事情的另一种方法”时，你都在非正式地思考等价性。这种推断在几种常见的情况下都会出现：

• 代码维护：你能在不改变程序其他部分行为方式的情况下简化、清理或重组代码吗？
• 向后兼容：你能在不改变任何现有功能工作方式的情况下增加新的功能吗？
• 优化：你能用更快或更节省空间的实现来取代代码吗？
• 抽象性：外部客户能看出我是否对我的代码做了这个改动吗？

还要注意的是，我们在前面的讲座中使用限制性签名，主要是为了等价：通过使用更严格的接口，我们让更多不同的实现变得等价，因为客户端无法分辨出区别。

我们想要一个精确的等价定义，这样我们就可以决定某些形式的代码维护或签名的不同实现是否真的可以。我们不希望这个定义过于严格，以至于我们不能进行修改以改进代码，但我们也不希望这个定义过于宽松，以至于用一个 “等价”的函数替换一个函数会导致我们的程序产生一个不同的答案。希望学习等价的概念和理论能够改善你看待用任何语言编写的软件的方式。

有许多不同的可能的定义，它们以略微不同的方式解决这种严格/宽松的矛盾。我们将专注于一个有用的、被设计和实现编程语言的人普遍认为的定义。我们还将简化讨论，假设我们有一个函数的两个实现，我们想知道它们是否等价。

我们的定义背后的直觉是这样的：

• 如果一个函数f与一个函数g（或类似的其他代码片断）产生相同的答案，并具有相同的副作用，无论它们在任何程序中以任何参数被调用，都是等价的。

• 等价性不需要相同的运行时间、相同的内部数据结构的使用、相同的辅助函数等等。所有这些东西都被认为是”不可观察的”，即不影响等价性的实现细节。

作为一个例子，考虑两种非常不同的列表排序方式。只要它们对所有的输入都产生相同的最终答案，那么不管它们在内部是如何工作的，或者其中一个是否更快，它们仍然可以是等价的。但是，如果它们对某些列表的行为不同，也许是对有重复元素的列表，那么它们就不是等价的。

然而，上面的讨论是通过隐含地假设函数总是返回并且除了产生答案之外没有其他作用而简化的。更确切地说，我们需要这两个函数在相同的环境下给出相同的参数：

1. 产生相同的结果（如果它们产生一个结果）
2. 具有相同的（非）终止行为；也就是说，如果一个永远运行，另一个也必须永远运行
3. 以相同的方式突变相同的（客户可见的）内存
4. 做同样的输入/输出
5. 引发相同的异常

这些要求都很重要，因为我们知道，如果我们有两个等价的函数，我们可以用另一个函数替换其中一个，程序中任何地方的使用都不会有不同的表现。

无副作用编程的另一个好处

要确保两个函数有相同的副作用（突变引用，进行输入/输出等），一个简单的方法是根本没有副作用。这正是ML等函数式语言所鼓励的。是的，在ML中，你可以让一个函数主体突变一些全局引用或其他东西，但这通常是不好的风格。其他函数式语言是纯函数式语言，这意味着在（大多数）函数中真的没有办法进行突变。

如果你”保持功能化”，不在函数体中进行突变、打印等，作为一个政策问题，那么调用者就可以假设很多其他方式无法实现的等价关系。例如，我们可以把(f x)+(f x)替换成(f x)*2吗？一般来说，这可能是一件错误的事情，因为调用f可能会更新一些计数器或打印一些东西。在ML中，这也是可能的，但作为一个风格问题，可能性要小得多，所以我们倾向于让更多的东西成为等价物。在一个纯粹的函数式语言中，我们保证替换不会改变任何东西。总的来说，当你试图决定两段代码是否等价时，突变真的会妨碍你的工作——这是避免突变的一个重要原因。

在维护无副作用的程序时，除了能够删除重复的计算（如上面的(f x)），我们还可以更自由地重新排列表达式。例如，在Java、C等语言中：

int a = f(x);
int b = g(y);
return b - a;

可能会产生与以下不同的结果：

return g(y) - f(x);

因为f和g可以以不同的顺序被调用。同样，这在ML中也是可能的，但如果我们避免副作用，这就不太可能了。（然而，我们可能仍然需要担心不同的异常被抛出和其他细节）。

标准等价

等价是很微妙的，特别是当你试图决定两个函数是否等价而不知道它们可能被调用的所有地方时。然而，这种情况很常见，比如你在编写一个未知客户可能使用的库时。我们现在考虑几种在任何情况下都能保证等价的情况，所以这些都是很好的经验法则，也是对函数和闭包如何工作的很好提醒。

首先，回忆一下我们已经学过的各种形式的语法糖。我们总是可以在函数体中使用或不使用语法糖，并得到一个等价的函数。如果我们不能，那么我们所使用的结构体实际上就不是语法糖。例如，不管g被绑定在什么地方，f的这些定义是等价的：

fun f x = 
    if x 
    then g x
    else false

fun f x =
    x andalso g

但请注意，如果g可能有副作用或不终止，我们不一定能用if g x then x else false来代替x andalso g x。

其次，我们可以改变一个局部变量（或函数参数）的名称，只要我们一致地改变它的所有用途。例如，这两个f的定义是等价的：

val y = 14 
fun f x = x+y+x

val y = 14
fun f z = z+y+z

但有一条规则：在选择新的变量名时，不能选择函数体已经在使用的变量来指代其他东西。例如，如果我们试图用y代替x，就会得到fun y = y+y+y，这与我们开始使用的函数不一样。一个以前未使用过的变量从来不是一个问题。

第三，我们可以使用或不使用辅助函数。例如，g的这两个定义是等价的：

val y = 14
fun g z = (z+y+z)+z 

val y = 14
fun f x = x+y+x
fun g z = (f z)+z

同样，我们必须注意不要因为f和g有潜在的不同环境而改变变量的含义。例如，这里g的定义是不等价的：

val y = 14
val y = 7
fun g z = (z+y+z)+z

val y = 14
fun f x = x+y+x
val y = 7
fun g z = (f z)+z

第四，正如我们之前用匿名函数解释的那样，不必要的函数包装是很差的风格，因为有一个更简单的等价方法。例如，fun g y = f y和val g = f总是相等的。然而，又一次出现了一个微妙的复杂情况。当我们有一个像f这样的变量与我们正在调用的函数绑定时，这个方法是有效的，但在更普遍的情况下，我们可能有一个表达式，它被评估为一个我们随后调用的函数。对于任何表达式e来说，fun g y = e y和val g = e总是相同的吗？不是的。

作为一个愚蠢的例子，考虑fun h() (print "hi" ; fn x => x+x)和e是h()。那么fun g y = (h()) y是一个每次被调用都会打印的函数。但val g = h()是一个不打印的函数——程序在为g创建绑定时将打印”hi“一次。这不应该是神秘的：我们知道val绑定”立即”评估其右手边，但函数体在被调用前不会被评估。

一个不太愚蠢的例子是，如果h可能引发一个异常，而不是返回一个函数。

第五，let val p = e1 in e2 end几乎可以成为(fn p => e2) e1语法糖。毕竟，对于任何表达式e1和e2以及模式p，这两段代码：

• 将e1评估为一个值
• 将该值与模式p匹配
• 如果匹配，将e2评估为由模式匹配扩展的环境中的一个值
• 返回评估e2的结果

由于这两段代码”做”的是完全相同的事情，它们必须是等价的。在Racket中，情况会是这样的（语法不同）。在ML中，唯一的区别是类型检查器：p中的变量在let-版本中允许有多态类型，但在匿名函数版本中不允许。

例如，考虑let val x = (fn y => y) in (x 0, x true) end。这个愚蠢的代码进行了类型检查并返回(0, true)，因为x的类型是'a->’a。但是(fn x => (x 0, x true)) (fn y => y)并没有进行类型检查，因为我们不能给x提供非多态的类型，而且函数参数不能有多态的类型。这就是ML中类型推断的工作方式。

重新审视我们的”等价物”定义

根据设计，我们对等价的定义忽略了一个函数需要多少时间或空间来评估。因此，两个总是返回相同答案的函数可以是等价的，即使一个花了一纳秒，另一个花了一百万年。从某种意义上说，这是一件好事，因为这个定义可以让我们用纳秒版本取代百万年版本。

但显然其他定义也很重要。数据结构和算法课程研究渐进复杂度，正是为了将一些算法区分为”更好的”（这显然意味着一些”差异”），即使这些更好的算法产生相同的答案。此外，渐进复杂度在设计上忽略了在某些程序中可能很重要的”恒定因素开销”，所以这种更严格的等价定义可能又太宽松了：我们实际上可能想知道两个实现所花的时间”差不多”。

这些定义中没有一个是优越的。所有这些都是计算机科学家一直在使用的有价值的观点。可观察的行为（我们的定义）、渐进复杂性和实际性能都是从事软件工作的人几乎每天都会使用的智力工具。