Impredicative polymorphism in F#

Question

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#?

Answer 1

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)