将ML代码转换为F#(更高通道的多态性)

Question

我正在尝试跟进"Lightweight high-kinded polymorphism"(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#中是不可用的.值得庆幸的是,这只是对(价值)去功能化概念的介绍的一部分,所以我认为这对你关心的论文部分并不重要.

另外,这里显示了使用更高级别类型的语言编码GADT的一种方法,因此您可以使用"轻量级高通道多态"方法实际编码GADT.

另外,更简单的,方法是展示了"简单化GADTs"一节在这里,其中大部分是直白地翻译成F#.然而,请注意那里提到的警告,莱布尼兹原则并不完全支持(并且查看页面的其他部分以查看再次需要更高种类的方法的优越扩展).