ML中的空列表是什么类型？

Question

我想知道 SML 中空列表的类型到底是什么（我正在使用 PolyML）？当我输入[]解释器时，我会得到：

val it = []: 'a list

这正是我所期望的。但是，如果我输入：

fun f a = if a = 0 then [] else [[]];

然后我得到：

val f = fn: int -> 'a list list

这似乎暗示也[]有这种类型'a list list。这到底是如何运作的？

Answer 1

在机器学习术语中，值具有类型方案，而不是类型。类型方案是类型的集合。它是带有通配符的类型，通配符可以替换为任何类型。用类型替换通配符称为实例化类型方案。

\n\n

中'a list，'a是一个类型变量，即通配符。空列表[]可用于作为类型方案实例的任何类型'a list。也就是说，对于任何类型T，空列表的类型为T list。例如，空列表有类型int list和类型bool list和类型(int * int * int) list和类型int list list等等。所有这些类型都是类型方案的实例'a list。

\n\n

当一个变量出现多次时，必须一致地替换它。例如fn x => x（恒等函数）具有类型 schema 'a -> 'a；它有 typeint -> int和 typebool -> bool但没有 type int -> bool。具有类型方案的值也'a -> 'b将具有该类型。int -> bool

\n\n

一个值可以有多种类型\xe2\x80\x94\xc2\xa0，这是编程语言中的常见现象。核心 ML 语言的一个属性是，类型正确的值的类型集恰好是类型方案的实例集。这个属性称为principality：ML 的类型系统是principal。机器学习的具体实现往往有原则性的例外情况；例如，SML 由于运算符重载而出现异常（具有和fn x => x + x两种类型，并且重载解析规则导致编译器决定上下文是否不强加）。int -> intfloat -> floatint -> intfloat

\n\n

其主要类型方案包含至少一个变量的值被称为多态的。主要类型方案不包含变量的值被称为单态的。

\n\n

通配符可以替换为类型方案。这产生了另一个类型方案，它是原始集合的子集，即该类型方案是原始类型方案的较小类型方案（细化）。例如，该值[[]]具有类型方案：它具有任何类型的'a list list类型。有类型、类型、类型等。T list listT[[]]int list listbool list list(int * int * int) list list

\n\n

在有关 ML 的文献中，\xe2\x80\x9ctype\xe2\x80\x9d 通常与 \xe2\x80\x9ctype schema\xe2\x80\x9d 互换使用，因此通常说 \xe2\x80\x9c 为空列表类型为'a list\xe2\x80\x9d。在有关类型系统的文献中，\xe2\x80\x9ctype\xe2\x80\x9d 通常表示 ML 术语中所说的 \xe2\x80\x9ctype 方案\xe2\x80\x9d，以及其他术语，例如 \xe2\x80\x9cground type \xe2\x80\x9d 用于没有变量的类型。

\n