原文标题：Higher-kinded bounded polymorphism
作者：Oleg Kiselyov
原文链接：Higher-kinded Bounded Polymorphism
为了表达数据集合上的泛型操作，或嵌入有类型的 DSL（尤其是在 tagless-final 方法中），经常需要对类型构造器［type constructor］进行抽象，然后在之后才为类型构造器提供参数。通常情况下，被抽象的类型构造函数不是任意的，而必须是实现了特定的接口（比如抽象序列）——这就是所谓有界多态［bounded polymorphism］。
OCaml 并不直接支持高种类多态［High-Kinded Polymorphism］：OCaml 的类型变量只能包含类型，不能包含类型构造函数；如果不给类型构造函数应用正确数量的参数，它就无法出现在类型表达式中。尽管如此，OCaml 还是可以表达高种类多态的——事实上，有几种或多或少比较麻烦的方式，其中的不那么麻烦的方式尤其鲜为人知，却又不断被重新发现。本文总结了表达（有些时候，是避免）高种类多态的不同方法。这些方法收集自多年以来的学术论文和 Caml-list 邮件列表上的信息，并根据文章的需要进行了调整和重新解释。
导言
Polymorphism abstracts types, just as functions abstract values. Higher-kinded polymorphism takes things a step further, abstracting both types and types constructors, just as higher-order functions abstract both first-order values and functions.
译：多态是类型的抽象，正如函数是值的抽象。而高种类多态则更进一步，它同时抽象了类型和类型构造函数——正如同高阶函数同时抽象了一阶值和函数。——Yallop 与 White（FLOPS 2014）
我们将进一步阐述这一非常精炼的总结，从而说明（有界的）高种类多态是如何产生的。这里介绍的例子将贯穿全文所有章节。
在实践中，经常会出现「对某些数字求和」的情况，对具体的数字类型进行抽象，就可以得到能在任意一个数字集合（列表）上执行的函数：
let rec sumi : int list -> int = function [] -> 0 | h :: t -> h + sumi t
我们可以进一步抽象 0 和 + 运算，由于它们本身就是函数（也可以说是一个带参数的值），结果就会得到一个高阶函数：
let rec foldi (f: int->int->int) (z: int) : int list -> int =
function [] -> z | h::t -> f h (foldi f z t)
在浮点数之类的列表上进行 fold 也具有类似的过程。那么，我们将进一步抽象——这次不是对值抽象，而是对类型 int 抽象。我们用一个类型变量替换具体的类型：
let rec fold (f: 'a->'a-'a) (z: 'a) : 'a list -> 'a =
function [] -> z | h::t -> f h (fold f z t)
这样就得到了所谓多态函数［polymorphic function］。多态函数描述了一种在不同类型的值组成的列表之上的统一进行的运算。运算 f 和值 z 可以放入这个多态记录类型中
type 'a monoid = {op: 'a->'a->'a; unit: 'a}
之前的 fold 就可以改写成
let rec foldm (m: 'a monoi) : 'a list -> 'a =
function [] -> m.unit | h::t -> m.op h (foldm m t)
当在某个 t list 类型的具体列表上 foldm 时，编译器会用列表中的类型 t 来初始化变量 'a。我们不可以传入完全随意的类型：必须存在一个与类型对应的，t monoid 类型的值，以作为 foldm 的参数。我们可以提出「 t 类型必须（至少）实现/支持 'a monoid 接口」，而 t monoid 类型的值就是这一命题的证明。因此 foldm 中的多态是有界的。
练习 1. 如果 'a monoid 真的是一个数学上的幺半群［Monoid］，那么应该有 op x unit = x 成立。利用这一特性，写出一个更加优化的 foldm（及后续变体）。
文件、字符串、数组、序列……都可以用同样的方法来 fold——只要支持对应的「解构」操作，任何集合都可以 fold。解构操作可以判断集合是否为空，或者给出集合中的一个元素，以及除此之外的剩余部分集合。我们想对这一点再次抽象：这次不是对 int 或 int list 这样的单纯类型抽象，而是对 list 这样的类型构造函数抽象，因此我们有
type ('a, 'F) seq = {decon: 'a 'F -> ('a * 'a 'F) option}
这是一段假想的 OCaml 代码：类型变量 'F（大写）不能用类型实例化，而要用「单参数的类型构造函数」来实例化。从技术上，我们称它具有更高的种类［kind］* -> *，这不同于类型和普通类型变量（如 'a）所具有的普通种类 *。因此，记录类型 seq 就成了高种类多态类型，这样可以将 foldm 函数进一步推广为
let rec folds (m: 'a monoid) (s: ('a, 'F) seq) : 'a 'F -> 'a = fun c ->
match s.decon c with None -> m.unit | Some (h,t) -> m.op h (folds m s t)
同理，我们也不能用任意类型构造器来实例化 'F，必须找到对应的 ('a, 'F) seq 类型值。folds 展示了所谓有界高种类多态。
可惜，在 OCaml 中无法使用这种具有更高种类的类型变量，下一节就会解释具体的原因。而本文接下来的章节中将阐述我们可以在 OCaml 中做什么来替代这种多态。我们提出了几种替代方案，在某些替代方案中，最终实现的结果几乎与上述的假想高种类多态代码完全一致。
为什么 OCaml 不能直接支持高种类多态？
Yallop 与 White 的 FLOPS 2014 论文（第 1.1 节）解释了 OCaml 不支持高种类类型变量的原因：一言以蔽之，类型别名问题。为完整起见，本节将在稍作改动的前提下复述他们的解释。
考虑下面两个模块：
module Tree = struct
type 'a t = Leaf | Branch of 'a t * 'a * 'a t
end
module TreeA : dcont = struct
type 'a t = ('a * 'a) Tree.t
end
这里的 'a Tree.t 是一种数据类型：它是一种全新的类型，不同于所有其他现有类型的类型。而 'a TreeA.t 是一个类型别名：正如其类型声明所展示的，它等于一个现有的类型： ('a * 'a) Tree.t。
我们先假设 OCaml 有高种类类型变量 * -> *，譬如上一节所假设的 'F。所谓类型检查，本质上就是求解/检查形如 'a 'F = 'b G 的类型方程。如果高种类类型变量中只涉及数据类型构造函数，那么求解就很简单了：'a = 'b 和 'F = 'G——数据类型总是「全新」的，只能等于它自己。这就是 Haskell 中的情况，Haskell 编译器会跟踪类型别名，甚至是跨越模块边界的类型别名，这么做只为确保：只有数据类型构造函数才能用于替换高种类类型变量1。Haskell 中的模块系统非常简单，因此这种跟踪不成问题。
相比之下，ML 的模块系统就复杂多了：它有函数、签名等等内容，而且广泛依赖于类型别名。试举一例：
module F(T: sig type 'a t val empty: 'a t end) = struct
type 'a ft = 'a T.t
end
如果禁止用类型别名来替换某高种类类型变量，就会严重限制类型系统的表达能力。例如，上面的 'a ft 是类型别名，因此 F(TRee).ft 就不能用于替换某高种类类型变量——但是程序员会觉得 F(TRee).ft 与 Tree.t 是一样的，后者却又可以这么替换。
另一方面，如果允许用类型别名来替换高种类类型变量，就会打破 'a 'F = 'b 'G 与 'a = 'b, 'F = 'G 之间的等价性。考虑 (int*int) 'F = int 'G，该方程有解 'F = Tree.t 和 'G = TreeA.t。像 'a TreeA.t 这样的有参数类型别名其实也是一种类型函数，而 int TreeA.t 则是这种函数的应用：将函数代入方程右侧，并用 int 替换 'a 就可得到。有了类型别名，判断类型相等的问题就变成了高阶统合［high-order unification］问题，而高阶统合问题是已知不可判定的2。
引用文献
- Jeremy Yallop and Leo White: Lightweight higher-kinded polymorphism
发表于 FLOPS 2014。
用 Functor 实现高种类函数
尽管 OCaml 不支持高种类类型变量，但要实现高种类多态也并非不可能。还有其他方法可以把类型构造器作为参数，第一个想到的就是 OCaml 的模块系统抽象（functor）。不过，这种方法相当繁琐，让我们一探究竟。
我们将要用真正的 OCaml 代码重写《导言》一节末尾处假设的高种类多态 OCaml 代码。具体做法是：提升等级——从项等级提升到模块级。上文所假设的记录类型
type ('a, 'F) seq = {decon: 'a 'F -> ('a * 'a 'F) option}
现在变成了模块签名
module type seq_i = sig
type 'a t
val decon : 'a t -> ('a * 'a t) option
end
这样就能用普通的类型构造器 t（类型常量）来表示 OCaml 中所不支持的高种类类型变量 'F。seq_i 接口的不同实现会以它们自己的不同方式来实例化 'a t（见下文的 ListS 等），t 的实际效果就像一个类型变量。上文假想的高种类多态函数
let rec folds (m: 'a monoid) (s: ('a, 'F) seq) : 'a 'F -> 'a = fun c ->
match s.decon c with None -> m.unit | Some (h,t) -> m.op h (folds m s t)
现在变成了以 seq_i 签名为参数的 functor：
module FoldS(S:seq_i) = struct
let rec fold (m: 'a monoid) : 'a S.t -> 'a = fun c ->
match S.decon c with None -> m.unit | Some (h,t) -> m.op h (fold m t)
end
这样就得到了我们所想要的：对序列进行抽象。要用这一设施来定义其他高种类多态函数：比如的序列求和的 sums，我们又需要 functor。某种意义上来说，functor 具有传染性。
module SumS(S:seq_i) = struct
open S
open FoldS(S)
let sum : int t -> int = fold monoid_plus
end
最后，来看一个实例化和使用高种类多态函数的例子：对列表求和。首先我们需要列表的的 seq_i 实例，这一实例证明了列表也是一种抽象序列。
module ListS = struct
type 'a t = 'a list
let decon = function [] -> None | h::t -> Some (h,t)
end
可以将其传递给 SumS functor
let 6 =
let module M = SumS(ListS) in M.sum [1;2;3]
附带代码中展示了另外一个例子：使用相同的 SumS 对数组求和。数组也是一种抽象序列。
总而言之，在这种方法中，所有高种类多态函数都是 functor。这导致了代码冗长、笨拙，充满了繁复的模板。例如，我们甚至不能把应用 SumS 写成 SumS(ListS).sum [1;2;3]，而必须使用上面给出的冗长的表达式。
引用文献
包含了测试以及其他示例的完整代码。
Yallop 与 White 的轻量级高种类多态
也许会令人惊讶的一点是，高种类多态总是可以还原成普通多态。Yallop 与 White 的 FLOPS 2014 论文就巧妙地展示出了这一点。他们将他们的方法称为去函数化［defunctionalize］。在此，将以另一种方式复述和解释他们的方法。
回顾类型 'a list，这是一个有参数的类型：'a 代表元素类型，list 代表集合的名称——可称之为「基本名」。要表达元素类型与基本名的组合，可以有很多种不同方法：如 ('a, list_name) app。其中 ('a, 'b) app 是一种固定类型，而 list_name 是某种代表基本名的普通类型。下面的双射证明了这两种表示法之间等价
inj: 'a list -> ('a,list_name) app
prj: ('a,list_name) app -> 'a list
这里指出一种实现这一双射的方法：首先，我们引入专用的「配对」数据类型，这种类型应是可扩展的，可以按需要定义任意多的配对。
type ('a,'b) app = ..
对于 'a list 有：
type list_name
type ('a,'b) app += List_name : 'a list -> ('a,list_name) app
这种情况下，'a list <-> ('a,list_name) app 的双射为：
let inj x = List_name x and
let prj (List_name x) = x
这两个函数显然互为反函数
练习 2. 事实上，要证明上面 inj 与 prj 互为反函数并不那么简单，需要一个附加条件。在我们的情况下，这一条件是满足的，请指出这一条件。
在我们的多态列表新表示法 ('a,list_name) app 中，基本名 list_name 是普通类型（种类为 * 的类型），对其抽象很简单：改成类型变量。基本名的多态就是普通多态。这样，就可以把《导言》一节末尾的多态抽象序列代码写成下面的 folds：
type ('a,'n) seq = {decon: ('a,'n) app -> ('a * ('a,'n) app) option}
let rec folds (m: 'a monoid) (s: ('a,'n) seq) : ('a,'n) app -> 'a = fun c ->
match s.decon c with None -> m.unit | Some (h,t) -> m.op h (folds m s t)
我们不写 'a 'F，而是写 ('a,'n) app，就这么简单。在其他高种类函数中使用 folds 也很直观：假设它是一个普通多态函数就好了（它确实就是一个普通多态函数）
let sums s c = folds monoid_plus s c
(* val sums : (int, 'a) seq -> (int, 'a) app -> int = <fun> *)
类型标注根本不必要，可以自动推导出类型。下面是一个实战例子：用该函数对列表求和
let list_seq : ('a,list_name) seq =
{decon = fun (List_name l) ->
match l with [] -> None | h::t -> Some (h,List_name t)}
let 6 = sums list_seq (List_name [1;2;3])
但仍有一点不便：用户必须自己写出基本名（如 list_name）和标签（如 List_name），并确保它们是唯一的。Yallop 与 White 利用模块系统实现了自动化，具体请参阅本页附带的代码，或 Yallop 与 White 的论文（以及 Opam 软件包 higher）。
本文稍后将从另一个角度再次讨论 Yallop 与 White 的方法，并实现之。
绕过高种类多态
有时，完全可以避免高种类多态：仔细观察后可能会发现，解决手头上的问题实际上并不需要高种类多态。事实上，我们使用的例子就是这样。
观察抽象序列接口，可以发现它以序列的元素类型和序列本身的类型为参数。我们首先想到的，但是不能在 OCaml 中写出来的定义是（取自《导言》一节）
type ('a,'F) seq = {decon: 'a 'F -> ('a * 'a 'F) option}
它有个特点：decon 操作会消费和生产相同 'a 'F 类型的序列（即输入和输出的类型完全一样）。也就是说，'F 总是作为 'a 'F 类型的一部分，而 'a 又是 seq 的参数：'a 与 'F 并不会独立发生变化。因此，这里并没有高种类多态，可以简单的把抽象序列的接口写成
type ('a,'t) seq = {decon: 't -> ('a * 't) option}
这样就可以完全按我们想要的形式来写 folds
let rec folds (m: 'a monoid) (s: ('a,'t) seq): 't -> 'a = fun c ->
match s.decon c with None -> m.unit | Some (h,t) -> m.op h (folds m s t)
就是普通的多态函数，用来定义其他的序列多态函数也毫无问题
let sums s c = folds monoid_plus s c
(* val sums : (int, 'a) seq -> (int, 'a) app -> int = <fun> *)
然后应用到列表上：
let list_seq : ('a,'a list) seq =
{decon = function [] -> None | h::t -> Some (h,t)}
let 6 = sums list_seq [1;2;3]
练习 3. 在假想的，支持高种类类型变量的 OCaml 中考虑集合的「映射」接口：
type ('a,'b,'F) ftor = {map: ('a->'b) -> ('a 'F -> 'b 'F)}
现在，用不同的类型实例化 'F。这一接口还能用普通多态表达吗？还是真的需要高种类多态？
仔细观察高种类多态接口 ('a,'F) seq 和普通多态接口 ('a,'t) seq，不难发现后者要更「大」一些：高种类接口只能描述形如 'a list 的多态序列，而 ('a,'t) seq 也适用于文件、字符串、缓冲区等等。这里我们欢迎这样的扩展：我们可以把同样的 folds 应用于某些针对其元素类型而优化了结构的序列。在 Haskell 中， ('a,'t) seq 是所谓的数据家族［data family］扩展3。下面是一个将 folds 应用于字符串的示例，注意字符串不是多态序列：
let string_seq : (char,int*string) seq =
{decon = fun (i,s) ->
if i >= String.length s || i < 0 then None else Some (s,[i], (i+1, s))}
let 'c' = folds monoid_maxchar string_se (0,"bca")
因此，我们可以将 folds 用于任何集合——无论集合本身是否多态，只要有 ('a,'t) seq 接口的实现就够了。我们发现了一项很古老，但是十分有用的技巧：我们可以在拓宽类型的同时，限制其真正可能有的值——通过定义「证据」（如 ('a,'t) seq）来实现这一点。
练习 4. Yallop 与 White 的方法也可以处理非多态集合，用它来实现上面的 string_seq。
代数
上面的 seq 接口例子，是关于如何解构序列的——从技术的角度而言，是一种共代数［coalgebra］。现在来研究构造：使用一组固定的操作来构造值，这一点可以被视为嵌入 DSL。为了抽象 DSL 的不同实现，就不得不引入多态；而如果嵌入的 DSL 是有类型的，那么这种多态就会变成高种类多态。在 tagless-final DSL 嵌入中，这种例子很常见。
在此，我们简要介绍下嵌入 DSL 是如何产生高种类多态，以及如何隐藏这些多态性。关键思想在于初始代数［initial algerba］4——根据定义，初始代数是对相同签名的其他任何具体代数的抽象，即对 DSL 实现的抽象。
本节使用的例子是一种支持整数和布尔值的简单编程语言，它就是 Pierce 的 «Types and Programming Languages» (TAPL) 中第 3 章使用的语言的一种方言。下面是这一语言在在 OCaml 中的 tagless-final 式嵌入（我们应该对此感觉很熟悉），用 OCaml 模块签名来表示该语言的语法：
module type sym = sig
type 'a repr
val int : int -> int repr
val add : int repr -> int repr -> int repr
val iszero : int repr -> bool repr
val if_ : bool repr -> 'a repr -> 'a repr -> 'a repr
end
这种语言有类型，因此表示 DSL 的项的类型 'a repr 会以项本身的类型（int 或 bool）为索引。签名 sym 也定义了 DSL 的类型系统：与 TAPL 中定义的几乎完全一样，但为了节省版面，我们的具体排版与 TAPL 有所不同。
下面是一个 DSL 中的项：
module SymEx1(I:sym) = struct
open I
let t1 = add (add (int 1) (int 2)) (int 3) (* 中间绑定 *)
let res = if_ (iszero t1) (int 0) (add t1 (int 1))
end
它是一个以 sym 为参数的 functor，这意味着我们抽象出了 DSL 的具体实现。DSL 项对于 sym 多态，所以可以在任意 DSL 实现中求值。由于 sym 中包含了高种类类型 repr，因此就带来了高种类多态。
方才介绍的（tagless-final 式）DSL 嵌入则遵循了《用 Functor 实现高种类函数》一节中描述的方法。实际上，我们从未完全摆脱 functor，只不过是利用了头等模块特性将其隐藏在项中。正如我们所见，类型为 int 的 DSL 项，比如 SymEx1 就是一个 functor
functor (I:sym) -> sig val res : int I.repr end
为了对 int 抽象，我们将其包装进模块里
module type symF = sig
type a
module Term(I:sym) : sig val res : a I.repr end
end
然后就可以将其转化为典型的多态类型
type 'a sym_term = (module (symF with type a = 'a))
这样就可以用普通 OCaml 值来表示 functor SymEx1：
let sym_ex1 : _ sym_term =
(module struct type a = int module Term = SymEx1 end)
这里需要添加类型注解，不过我们可以用 _ 替代，OCaml 会自动推导出它为 int。假设有一个 sym 的实现叫做模块 R，我们可以用它来运行以下例子（并通过 R 的解释获得 sym_ex1 的值）：
let _ = let module N = (val sym_ex1) in
let module M = N.Term(R) in M.res
'a sym_term 类型本身也可以一种「车轱辘话」式的方法来实现 sym 签名：
module SymSelf : (sym with type 'a repr = 'a sym_term) = struct
type 'a repr = 'a sym_term
let int : int -> int repr = fun n ->
let module M(I:sym) = struct let res = I.int n end in
(module struct type a = int module Term = M end)
let add : int repr -> int repr -> int repr = fun (module E1) (module E2) ->
let module M(I:sym) =
struct module E1T = E1.Term(I) module E2T = E2.Term(I)
let res = I.add (E1T.res) (E2T.res)
end in
(module struct type a = int module Term = M end)
...
end
真是拗口，但是这样摆脱了 functor 和类型注解，写 sym DSL 就简单多了。之前的 sym_ex1 现在可以写成
let sym_ex1 =
let open SymSelf in
let t1 = add (add (int 1) (int 2)) (int 3) in (* 中间绑定 *)
if_ (iszero t1) (int 0) (add t1 (int 1))
这段 DSL 也可以在 R 或者其他 DSL 实现中求值。
从技术上讲，SymSelf 是一种初始代数：对于任何其他实现，它都有唯一一种映射到该实现上的方式。这意味着 sym_ex1 等项可以在任何 sym DSL 实现中求值，它对于 DSL 实现多态。
从坏的方面看，SymSelf 是这种琐碎而大量的模板代码的缩影；而从好的方面看，它大大简化了编写 DSL 的过程：没有类型注解、没有 functor、没有实现传递，也没有公开的多态需求，无论是高种类多态还是普通多态。但是这些项仍可以在任意 DSL 实现中求值。
练习 5. 将 Yallop 与 White 的方法应用于这个 DSL 示例（提示：Yallop 与 White 论文中的第一个示例——Monad 表示法就是一种 tagless-final DSL 嵌入）。
引用文献
带测试和详细开发细节的完整代码
展示了如何使用头等 functor 来构造单类别代数的初始代数（对应于无类型 DSL）
- Stephen Dolan: phantom type.
于二〇一五年四月二十七日星期一 12:51:11 发布于 caml-list 邮件列表上。
高种类类型名字的本质
现在，我们从另一个角度来看待 Yallop 和 White 的将高种类多态还原成普通多态的方法。即便这不能提供新的见解，至少也能提供新的实现方法。
像 'a list 这样的多态类型代表了：以某个类型（本例中是列表元素的类型）为索引的类型家族［type family］。假想 OCaml 中的 'a 'F 这样的高种类类型变量 'F 可以说是一种：在保留索引的同时，对类型家族名称进行抽象。下面是实现这种抽象的另一种方法。
考虑存在量化类型［existential type］：exist a. a list（在 OCaml 中可以通过多种方式实现，不过具体符号会有所不同；为了清晰起见，我们决定保留这一符号）。存在量化类型现在是普通的、种类为 * 的类型，可以用类型变量（如 'd）来抽象。因此「类型家族名」就可以表示为类型家族本身加上其中隐藏的索引。然而，我们现在已经失去了索引；那么，我们就将其拼回，最终得到类型 ('a, 'd) hk。因此对于任意类型 t，(t, exist a. a list) hk 和 t list 等价。
但问题在于：('a,'d) hk 是一个范围更广的类型，而我们需要存在量化类型中隐藏的索引恰好是 t——我们需要依值对［dependent pair］，但 OCaml 不支持。不过，别忘了那个古老的技巧：只要我们控制值的制造者，确保只能制造出满足条件的值，那么更大的类型也无妨。具体来说，我们必须确保只能通过形如 inj: 'a list -> ('a, exists a. a list) hk 这样的函数来制造 ('a, 'd) hk 类型的值，因为这样的函数才知道其中隐含的具体索引。
而某些时候，类型检查器会要求你证明存在对应的反函数 ('a, exists a. a list) hk -> 'a list，才能从存在量化类型中提取出真正的列表。我们有几种方法可以证明这一点。最简单的方法就是口头承诺：对于所有 ('a, 'd) hk 值，这一条件都成立，而且我们在纸上或者某些 .v 文件上有证明。这样就得到了一个异常简单的实现：什么都不做（两个方向的函数都是恒同函数）。
module HK : sig
type ('a,'d) hk (* 抽象类型 *)
module MakeHK : functor (S: sig type 'a t end) -> sig
type anyt (* 也是抽象类型 *)
val inj : 'a S.t -> ('a,anyt) hk
val prj : ('a,anyt) hk -> 'a S.t
end
end = struct
type ('a,'d) hk = 'd
module MakeHK(S:sig type 'a t end) = struct
type anyt = Obj.t
let inj : 'a S.t -> ('a,anyt) hk = Obj.repr
let prj : ('a,anyt) hk -> 'a S.t = Obj.obj
end
end
附带的代码中则展示了另一种不同的实现，也非常简单，而且不需要 Obj 魔法56。
在使用「伪造的高种类类型」为上节的 sym DSL 签名赋能后：
module type sym_hk = sig
include sym
include module type of HK.MakeHK(struct type 'a t = 'a repr end)
end
我们就可以把之前的 SymEx1 写成函数（项）而非 functor 了：
let sym_ex1 (type d) (module I:(sym_hk with type anyt=d)) : (_,d) HK.hk =
let open I in
let t1 = add (add (int 1) (int 2)) (int 3) |> inj in (* 中间项 *)
let res = if_ (iszero t1) (int 0) (add t1 (int 1)) in
inj res
可以简单地如下求值
sym_ex1 (module RHK) |> RHK.prj
RHK 是一个实现了 sym_hk 的模块，顺带一提，如果 SHK 是另一个实现 sym_hk 的模块，我们尝试 sym_ex1 (module RHK) |> SHK.prj 就会发现：(int,RHK.anyt) bk 和 (int,SHK.anyt) 实际是不同的类型，虽然 HK 在运行时什么都不做，但它确实维护了程序的安全与健全。
结论
我们研究了各种「对类型构造函数进行抽象」的方法——或者说是「当接口涉及多态类型时，编写『对接口参数化』的项」的方法。即便语言不支持类型构造函数上的多态，我们仍可以利用以下手段实现这种接口参数化：
用 functor 抽象实现接口抽象
通过在类型构造函数和普通类型间建立双射，从而将高种类多态还原成普通多态
将 DSL 实现多态隐藏在初始代数之下（如果接口是一种代数，在 tagless-final DSL 嵌入中，这很常见）
以及，在某些问题中，经过仔细的观察就可以发现：实际并不需要高种类多态。
参考
译者注：某种意义上，这也是 Haskell 中需要 newtype 构造的原因。 ↩︎
https://www.ps.uni-saarland.de/Publications/documents/SpiesForster_2019_UndecidabilityHOU.pdf ↩︎