В OCaml предполагаемый тип
let f = List.map fst
является
val f : ('_weak1 * '_weak2) list -> '_weak1 list = <fun>
в то время как предполагаемый тип
let g x = List.map fst x
является
val g : ('a * 'b) list -> 'a list = <fun>
(типы взяты из utop).
В результате f
нельзя использовать полиморфно, а g
можно.
Почему это эта-преобразование между чистыми функциями вызывает такую разницу в выводе типов?
похоже, что '_weak1
имеет особое значение в системе типов ocaml. Если вы попытаетесь выполнить f [(1,0); (2, 0)];; f [("a", 0); ("b", 0)]
, проверка типов завершится ошибкой, однако g [(1,0); (2, 0)];; g [("a", 0); ("b", 0)]
пройдет нормально
Разница возникает из-за ограничение стоимости, который не позволяет первому определению быть полиморфным: оно определяется приложением, которое не является значением. Вторая форма определяется как функция, которая является значением. Обозначение '_weakN
указывает на мономорфный тип, который еще не разрешен, в отличие от переменной полиморфного типа, такой как 'a
.
См. эта глава для получения дополнительной информации.
Большое спасибо за это! Я думаю, что в целом понимаю, однако меня смущает пункт "определяется приложением, которое не является значением" - значит ли это, что List.map fst
не является значением?
Значение в синтаксическом смысле, так что нет, приложение — это не значение, это выражение, вычисляющее значение. С другой стороны, лямбда является синтаксическим значением (типа функции).
Я бы подумал, что это точно такой же тип, просто использующий разные имена для переменных типа.