是否可以在标准 ML 中支持更高种类的类型？答案

【问题标题】：Is it possible to support higher-kinded types in Standard ML?是否可以在标准 ML 中支持更高种类的类型？
【发布时间】：2019-11-11 03:57:11
【问题描述】：

我在this post 中读到，机器学习方言不允许非地面类型的类型变量。例如。最后一条语句不可表示：

-- Haskell code
type Ground        = Int    
type FirstOrder  a = Maybe a
type SecondOrder c = c Int   -- ML do not allow :c

OCaml 仅在模块级别支持更高种类。有一些解释（here 和作者的评论here）关于 OCaml 的哪些功能与更高种类的类型机会发生冲突。

如果我理解正确的话，主要问题在于以下事实：

OCaml 不遵循类型定义的“新鲜度”限制：构造 type 可以定义别名（类型将保持不变）和新的新鲜类型
类型别名定义可以隐藏

AFAIK，标准 ML 对类型定义和别名有不同的构造：type 用于别名，datatype 用于新类型的引入。

不幸的是，我对 SML 的了解不够——是否可以导出类型别名并隐藏其定义？如果有任何其他 SML 功能仍然不能很好地适应更高种类的类型的机会，有人可以告诉我吗？

仿函数可能会出现一些问题——能否提供一个代码示例？这类案例我听过好几次了，但还是没有找到完整的例子。

【问题讨论】：

标签： sml language-design higher-kinded-types

【解决方案1】：

是的，SML 可以通过函子表达等价的高级类型，也可以将它们抽象化。没用的例子：

functor F (type 'a t) :> sig type 'a u end =
struct
    type 'a u = ('a t) t
end

但是，与 OCaml 不同，SML（官方）没有高阶仿函数，因此根据标准，您只能以这种方式表示二阶类型构造函数。

FWIW，OCaml 可以对类型别名和生成类型使用相同的关键字（type 与 SML 中的datatype），但它们在句法上仍然可以通过右侧进行区分。所以这与 SML 没有真正的区别。在这两种语言中，出现在签名中的抽象可以实现为类型别名或生成类型。因此，Leo 所暗示的类型推断问题同样存在于两者中。 Haskell 可以摆脱这个问题，因为它在类型抽象方面没有相同的表现力（即，没有模块的“密封”运算符）。

【讨论】：

我是否理解正确，如果我们禁止按原样导出类型别名以保证签名中的所有类型都是生成的，它会解决问题吗？看起来不是，我仍然错过了另一个矛盾点......我提到了 OCaml 中唯一类型引入关键字的特性，只是因为，即使前面的陈述是正确的并且想要禁止导出别名，这样做也会有点笨拙只有一个关键字（当然可以）。
@AlexanderBashkirov，是的，我认为如果 ML 不允许对非生成类型定义进行抽象，那么问题就会消失。但是，这会严重削弱语言，因此并不是真正的解决方案。
真的有这么多吗？只是在抽象它们之前用额外的datatype 包装所有别名。无论如何，从模块的外部角度来看，我们不能对抽象类型下的真实类型说任何话，可以吗？所以额外的包装不应该影响用户（据我所知）。但是对于类型系统知识来说，所有抽象类型的模块都是生成的（我觉得它甚至是自然的）。我不知道共享约束是否足够好，但我也没有看到它们有任何问题。
P.S.我以 OCaml 方式使用术语“共享约束”，在 SML 中它是 where type 子句，AFAIK。
@AlexanderBashkirov，这在高阶情况下不起作用，因为它需要深度复制——这反过来又将抽象限制为纯数据结构。作为一个简单的例子，假设签名{type t; val f : int list -> t list}，其中t 实现为int。或者g : int ref list -> t ref list，复制根本行不通。