Исходное сообщение
"Увидел свет язык программирования Rust 1.13" Отправлено 5kbps, 13-Ноя-16 02:49
> И кстати там не чистый HM. Там его расширили классами типов. И > если для HM есть строгая теория, доказывающая корректность этого разолвера, то > вот для этого расширения мне не известны доказательства корректности. Если они > есть, поправьте меня пожалуйста. А в чём проблема? Любой класс типов можно рассматривать как обобщающий тип. Разница лишь в том, что конкретизировать класс типов можно не в любой тип, а только в тот, для которого определены требуемые для данного класса типов функции. Но это не важно, потому что в правилах вывода типов не используется конкретизация типов вообще, только обобщение. Иными словами, HM + классы типов - это подмножество HM. ИМХО.