F#中的命令性多态性 [英] Impredicative polymorphism in F#

问题描述

OCaml的Hindley-Milner类型系统不允许强制性多态性(称为System-F)，除非最近对记录类型进行了扩展.同样适用于F#.

有时有时需要将强制性多态性(例如Coq)编写的程序翻译成此类语言. Coq提取到OCaml的解决方案是(部分地)使用Obj.magic，这是一种通用的不安全类型转换.之所以有效，是因为

• 在OCaml的运行时系统中，所有值的大小均相同，无论其类型如何(32位或64位，具体取决于体系结构)
• 应用于原始程序的更复杂的字体系统保证了字体的安全性.

是否可以在F#中做类似的事情?

解决方案

如果您可以详细说明要实现的目标，将很有帮助.一些强制性用法(例如Haskell中的此示例 wiki)相对容易通过单一通用方法使用其他标称类型进行编码:

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)

OCaml's Hindley-Milner type system does not allow for impredicative polymorphism (à la System-F), except through a somewhat recent extension for record types. The same applies to F#.

It however is sometimes desirable to translate programs written with impredicative polymorphism (e.g. Coq) into such languages. The solution for Coq's extractor to OCaml is to (sparingly) use Obj.magic, which is a kind of universal unsafe cast. This works because

• in OCaml's runtime system, all values have the same size regardless of their type (32 or 64 bits depending on architecture)
• the more sophisticated type system applied to the original program guarantees type safety.

Is it possible to do something similar in F#?

解决方案

It would be helpful if you could elaborate on exactly what you'd like to achieve. Some impredicative uses (such as this example from the Haskell wiki) are relatively easy to encode using an additional nominal type with a single generic method:

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)

这篇关于F#中的命令性多态性的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！