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

Caiman

Polymorphic record fields are not "recent" by most standards, as they were introduced in 2002 for 3.05. – Apheliotropic

It is worth mentioning that the meaning of "impredicative polymorphism" is different in the context of Coq. Coq does allow a type variable to be instantiated with a polymorphic type, but usually there are restrictions on when one can do so, even when the value is boxed. This is done to guarantee logical consistency. On the OCaml and Haskell side, what is being called "impredicative" is just being able to substitute an unboxed (i.e., not record) polymorphic type for a type variable. Thus, it is just a way to make higher-rank types more convenient. – Armadillo

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)

Carlynne

Here's another example I wrote a few months ago: gist.github.com/mausch/3895976 – Resplendent

The exact same thing can be done in OCaml with a record written as type forall_list = {apply : 'a. 'a list -> 'a list} and let rev = {apply = List.rev}. – Cockswain

Yes, this is the somewhat recent extension for record types that I alluded to (record fields may have universal types). – Caiman