F＃中的impredicative多态性-Java 学习之路

OCaml的Hindley-Milner类型系统不允许使用impredicative多态（àlaSystem-F），除非通过最近的记录类型扩展 . 这同样适用于F＃ .

然而，有时希望将用不可预测的多态性（例如Coq）编写的程序翻译成这些语言 . 针对OCaml的Coq提取器的解决方案是（谨慎地）使用 Obj.magic ，这是一种通用的不安全转换 . 这是因为

在OCaml的运行时系统中

，所有值都具有相同的大小，无论其类型如何（32位或64位，具体取决于体系结构）
应用于原始程序的更复杂的类型系统保证了类型安全 .

是否有可能在F＃中做类似的事情？

1 回答

如果你能详细说明你想要实现的目标，将会很有帮助 . 一些不可预测的用法（例如来自Haskell wiki的this example）使用一个通用方法使用额外的名义类型进行编码相对容易：

type IForallList =
    abstract Apply : 'a list -> 'a list

let f = function
| Some(g : IForallList) -> Some(g.Apply [3], g.Apply ("hello" |> Seq.toList))
| None -> None

let rev = { new IForallList with member __.Apply(l) = List.rev l }

let result = f (Some rev)

回复于 2024-05-08T07:11:38+08:00

F＃中的impredicative多态性

1 回答

相关问题