OCaml の Hindley-Milner 型システムは、レコード型のやや最近の拡張を除いて、非予測的ポリモーフィズム (システム F 風) を許可していません。同じことが F# にも当てはまります。
ただし、非予測的ポリモーフィズム (Coq など) で記述されたプログラムをそのような言語に翻訳することが望ましい場合もあります。OCaml に対する Coq のエクストラクタの解決策は、(控えめに) を使用することObj.magic
です。これは、ユニバーサル アンセーフ キャストの一種です。これは次の理由で機能します。
- OCaml のランタイム システムでは、すべての値は型に関係なく同じサイズです (アーキテクチャに応じて 32 ビットまたは 64 ビット)。
- 元のプログラムに適用されたより洗練された型システムは、型の安全性を保証します。
F# で同様のことを行うことは可能ですか?