Система типа OCaml Hindley-Milner не допускает неспецифического полиморфизма (à la System-F), за исключением нескольких недавних расширений для типов записей. То же самое относится к F #.
Однако иногда желательно перевести программы, написанные с помощью непроизводительного полиморфизма (например, Coq) на такие языки. Решение для экстрактора Coq для OCaml должно (экономно) использовать Obj.magic, что является своего рода универсальным небезопасным литьем. Это работает, потому что
- в системе времени исполнения OCaml, все значения имеют одинаковый размер независимо от их типа (32 или 64 бита в зависимости от архитектуры).
- более сложная система типов, применяемая к исходной программе, гарантирует безопасность типа.
Можно ли сделать что-то подобное в F #?
