Standard ML中，数据类型构造器是否属于值？

你的工作定义和SML标准里对值的定义是一致的：值是无法进一步约简的表达式，求值结果就是自身。基于这个前提，我们来逐个解答你的疑问：

1. SOME是不是严格意义上的函数？ #

不是。虽然SML/NJ的REPL给它标注的类型是'a -> 'a option，看起来像函数类型，但SOME是数据构造器，和函数有着本质区别：

• 函数是通过λ-抽象定义的，求值时需要进行β-归约（比如(fn x => x+1) 2会归约为3）；
• 数据构造器是用来创建代数数据类型实例的“构造工具”，它本身就是值，不需要归约，应用到参数时直接生成对应类型的值，不会执行任何计算逻辑。

2. SOME和SOME 1算不算值？ #

算。根据SML的标准值定义，以下都属于值：

• 基本常量（如1、true）；
• 数据构造器本身（包括SOME、NONE这类option类型的构造器，或者你自定义的datatype t = A | B of int里的A、B）；
• 数据构造器应用到值得到的实例（如SOME 1、B 5）；
• 函数抽象、元组、记录等复合结构。

SOME和SOME 1都无法进一步约简，求值结果就是自身，完全符合你对值的定义。

3. SOME是不是全函数？ #

是。这里的“全”指的是对任意类型'a的合法值x，SOME x都能得到一个值。因为SOME作为数据构造器，只要输入x是值，它就直接构造出'a option类型的实例，这个实例本身就是值，不存在求值失败、抛出异常或者无法归约的情况，所以SOME是全的——这一点确实可以由SOME x本身是值直接推导出来。

内容的提问来源于stack exchange，提问作者qwr