Как Rust решает проблему изменчивости для Хиндли-Милнера?

Я читал, что в Rust очень хороший вывод типов с использованием Hindley-Milner. В Rust также есть изменяемые переменные, и AFAIK должны быть некоторые ограничения, когда алгоритм HM работает с изменчивостью, потому что он может чрезмерно обобщать. Следующий код:

let mut a;
a = 3;
a = 2.5;

Не компилируется, потому что во второй строке было выведено целое число, и значение с плавающей запятой не может быть присвоено целочисленной переменной. Итак, я предполагаю, что для простых переменных, как только выводится неуниверсальный тип, переменная становится монотипом и больше не может быть обобщена.

А как насчет шаблона, такого как Vec? Например этот код:

let mut v;
v = Vec::new();
v.push(3);
v.push(2.3);

Это снова не удается, но снова для последней строки. Это означает, что вторая строка выводит тип частично (Vec), а третья - тип контейнера.

Какое правило? Есть ли что-то вроде ограничения ценности, о котором я не знаю? Или я слишком усложняю, а в Rust гораздо более жесткие правила (например, без обобщений)?


rust mutable hindley-milner
person Peter Lenkefi    schedule 10.05.2017    source источник
comment
Вам повезло, работа над выводом типа Rust продолжается, и Нико Мацакис ведет блог о своей работе над новым механизмом унификации: Unification in Chalk - Часть 1 и Unification in Chalk - Часть 2.   -  person Matthieu M.    schedule 10.05.2017
comment
@MatthieuM. Спасибо, я это прочитаю!   -  person Peter Lenkefi    schedule 10.05.2017

Ответы (2)


arrow_upward
5
arrow_downward

Считается проблемой (с точки зрения качества диагностики) то, что rustc слишком рьяно выбирает свой тип.

Если мы проверим ваш первый пример:

let mut a = 3;
a = 2.5;

Тогда первая строка приведет к выводу, что a имеет {generic integer type}, а вторая строка приведет к диагностике того, что 2.5 не может быть назначен на a, потому что это не общий целочисленный тип.

Ожидается, что лучший алгоритм вместо этого зарегистрирует конфликт, а затем укажет на строки, из которых произошел каждый тип. Может быть, мы добьемся этого с помощью Chalk < / а>.

Примечание: универсальный целочисленный тип - это уловка Rust, позволяющая сделать целочисленные литералы «полиморфными». Если нет других указаний на то, какой именно целочисленный тип должен быть, по умолчанию будет использоваться i32.

Второй пример происходит примерно так же.

let mut v = Vec::new();
v.push(3);

Подробно:

  • v присвоен тип $T
  • Vec::new() производит тип Vec<$U>
  • 3 производит тип {integer}

Итак, в первой строке мы получаем $T == Vec<$U>, а во второй строке мы получаем $U == {integer}, так что v имеет тип Vec<{integer}>.

Если нет другого источника для определения точного целочисленного типа, по умолчанию он возвращается к i32.

Я хотел бы отметить, что изменчивость здесь на самом деле не влияет на вывод; с точки зрения вывода типов или унификации типов следующие примеры кода эквивалентны:

//  With mutability:
let mut a = 1;
a = 2.5;

//  Without mutability:
let a = if <condition> { 1 } else { 2.5 };

В Rust есть гораздо более серьезные проблемы с HM, Deref и подтипами, которые намного сложнее.

person Matthieu M.    schedule 10.05.2017
comment
Я думаю, OP хотел знать, используют ли let mut привязки let-полиморфизм + ограничение синтаксического значения или просто используют мономорфные типы. - person max; 23.08.2018

arrow_upward
5
arrow_downward

Если я не ошибаюсь, он делает следующее:

let mut a;
a = 3;     //here a is already infered as mut int
a = 2.5;   //fails because int != float

Для фрагмента vec:

let mut v;
v = Vec::new();// now v type is Vec<something>
v.push(3);     // v type is Vec<int>
v.push(2.3);   // here fails because Vec<int> != Vec<float>

Обратите внимание, я не использовал типы ржавчины, а просто для общего представления.

person Netwave    schedule 10.05.2017
comment
То есть вы говорите, что в алгоритме не должно быть обобщений? - person Peter Lenkefi; 10.05.2017
comment
@PeterLenkefi, он обобщает, пока не найдет первый специализированный полный тип - person Netwave; 10.05.2017
comment
@PeterLenkefi Что вы имеете в виду под отказом от обобщения? v = Vec::new() фактически является ограничением, которое v: Vec<T> для некоторых T; v.push(3) - это ограничение, которое T = {integer} (в противном случае по умолчанию будет i32, если нет доказательств). Как можно было бы более обобщить любое из этих ограничений? - person trentcl; 10.05.2017
comment
@PeterLenkefi Важно помнить, что Rust не имеет иерархии типов чисел, поэтому Rust не может просто сделать его Vec<Number> или Vec<Rational> или что-то в этом роде. Ближайшим из них может быть Vec<&PartialOrd>, но создание чертобъектов могло бы имеют затраты времени выполнения, и Rust пытается сделать затраты времени выполнения явными. - person Wesley Wiser; 10.05.2017
comment
@trentcl без обобщения означает, что типы остаются мономорфными (то есть без универсальной количественной оценки, в отличие от let-полиморфизма HM) - person max; 23.08.2018