types - 将 ML 代码转换为 F#(更高级的多态性)

Question

我正在尝试跟进论文“轻量级高级多态性”(https://ocamllabs.github.io/higher/lightweight-higher-kinded-polymorphism.pdf)
我坚持将这个 ML 代码转换为 F#

type (_,_) arrow =
    Fn_plus : ((int ∗ int), int) arrow
    | Fn_plus_cons : int → ((int ∗ int list), int list) arrow

和

let apply : type a b. (a, b) arrow ∗ a → b =
    fun (appl, v) → match appl with
    | Fn_plus → let (x, y) = v in x + y
    | Fn_plus_cons n → let (x, l’) = v in x + n :: l’ 

具体来说，类型定义就像一堵巨大的魔法墙。

Answer 1

此示例使用 GADT(有点像可区分联合，其中单个联合案例可以以不同方式约束类型的参数)，而 F# 中不提供这些联合。值得庆幸的是，这只是对(值(value))去功能化概念的介绍的一部分，所以我认为这对您关心的论文部分实际上并不重要。

顺便说一句，显示了一种在具有更高级类型的语言中编码 GADT 的方法 here ，因此您实际上可以使用“轻量级高级多态性”方法本身对 GADT 进行编码。

另一种更简单的方法在“Simplistic GADTs”部分 here 中进行了演示。 ，这很容易转换为 F#。但是，请注意那里提到的警告，莱布尼茨原则并没有得到完全支持(并查看页面的其他部分以查看再次需要更高种类的方法的高级扩展)。