types - SML 中的值，具有有限数量的类型 n

对于 n=0 和 n=1，答案应该是明确的（零，很多）。

但是对于 n > 1 怎么办？

TL;DR：对于某些人来说，是的，但不是一般的。

让我了解这些明确的答案是否是：

n = 0：不，没有属于零类型的值。（如果一个值存在，它必须有一个类型。在定义它们的类型之前，值在 SML 中不存在。）
n = 1：是的，有一个值恰好属于一种类型。（有无数种方法可以表达一个只属于一种类型的值：datatype one = One, datatype two = One | Two, datatype three = One | Two | Three，在这种情况下，这些值构造函数中的任何一个在任何一点都只属于一种类型。）

如果这不是对您问题的正确解释，您能否澄清和详细说明问题以及这些明确的答案？继续假设这种解释是正确的，这里有一些关于 n > 1 的想法：

对于具有多种类型的值，该值必须是多态的。我可以想到两种方法：

对于“临时多态性”（又名重载）：n = K：一些有限的重载示例，具有多种类型的内置运算符（例如+，同时具有类型int * int -> int和real * real -> real，取决于推断的内容。）老实说，我不知道不确切知道有多少类型+为它重载，但我可以看到它至少是 3：
```
- 1 + 1;
> val it = 2 : int
- 1.0 + 1.0;
> val it = 2.0 : real
- 0w1 + 0w1;
> val it = 0wx2 : word
```
所以对于一些任意的 K ≥ 3：是的，op +是一个恰好具有 K 类型的值。

也许有多个具有不同类型数量的重载内置值，但由于只有有限多个重载内置运算符，这仅适用于极少数 n > 1，而不适用于所有 n > 1一般来说。

您可能会争辩说，这实际上是三个op +具有相同名称的不同值。它们的实现方式不同，行为也不同，因此可以合理地说它们不是相同的值，即使它们共享相同的名称。在这种严格的解释下，只剩下参数多态性了。
对于“参数多态”：值[]有 type 'a list，但也有 type int list, real list, bool list, 等等。我不知道你是否会说它有无限多种类型，但我想你可以这么说。但即使你确实这么说了，类型的值'a something也不会有有限数量的 n > 1 类型。也不是这样('a, 'b) something，依此类推。

除了这两种多态性之外，我想不出其他方法可以让一个值在 SML 中具有多种类型。一个有趣的后续问题是，除了这两种方式之外，是否存在有意义的方式来定义具有 n > 1 的 n 类型的任何类型系统中的值。

如果问题是“对于每个整数 n ≥ 0，是否存在恰好具有 n 个值的类型？” 答案是“是”，因为对于 n = 1 你有，对于 n = 2 你有，依此类推。对于 n = 0，您可以构造一个没有暴露构造函数的抽象/不透明类型。在 Haskell 中，这种类型没有任何部分，但在 SML 中缺少这种语法，您可以执行以下操作：datatype One = Onedatatype Two = One | Twodata Void= ...

signature VOID = sig type t end
structure Void :> VOID = struct type t = unit end

fun whyNot (x : Void.t) = "I wonder how one might call this function."

即使Void.t定义为unit，它也是不透明的，隐藏了()值构造函数：

- whyNot ();
! Toplevel input:
! whyNot ();
!        ^^
! Type clash: expression of type
!   unit
! cannot have type
!   Void.t

所以和之间的等价性Void.t没有unit暴露出来，给类型Void.t0 值。

types - SML 中的值，具有有限数量的类型 n > 1

问题描述

解决方案

推荐阅读