Imprädikativer Polymorphismus in F #

Question

Das Hindley-Milner-System von OCaml erlaubt keine imprädikative Polymorphie (à la System-F), außer durch eine etwas jüngere Erweiterung für Datensatztypen. Gleiches gilt für F #.

Es ist jedoch manchmal wünschenswert, mit imprädikativem Polymorphismus (z.B. Coq) geschriebene Programme in solche Sprachen zu übersetzen. Die Lösung für Coq's Extractor zu OCaml ist, (sparsam) Obj.magic zu verwenden, das eine Art universellen unsicheren Cast ist. Dies funktioniert, weil

• in OCaml der Runtime-System, alle Werte die gleiche Größe, unabhängig von ihrer Art haben (32 oder 64 Bit je nach Architektur)
• des anspruchsvolleren Art System zu dem ursprünglichen Programm angewandt garantiert Sicherheit geben.

Ist es möglich, etwas ähnliches in F # zu tun?

Answer 1

Es wäre hilfreich, wenn Sie genauer erläutern könnten, was Sie erreichen möchten. Einige imprädikative Anwendungen (wie this example vom Haskell wiki) sind relativ einfach einen zusätzlichen Nenn Typen mit einer einzigen generischen Methode zum Codieren mit:

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)