В чем разница между «а» и «_l»?

Question

В чем разница между 'a и '_l?

Я смотрел на эту ошибку и не мог ее понять:

Error: This expression has type ('a -> float polynomial) list but an expression was expected of type float polynomial list derivlist: ('_l → float polynomial) list

Answer 1

_ обозначает слабо полиморфную переменную: она находится в положении, где ее нельзя обобщить.

В FAQ по OCaml есть два объяснения, относящихся к слабому полиморфизму: см. Функция, полученная посредствомчастичное применение недостаточно полиморфно и следующее.

Это обычно происходит, когда вы используете нелокальную ссылку (тип которой не может быть обобщен) или когда определяются полиморфные функции, которые не являются синтаксическифункции (они начинаются не с fun x -> .., а с приложения функции).В некоторых случаях есть простое исправление (eta-расширение, см. FAQ), иногда его нет, а иногда ваша программа просто не работает.

Простой пример: let a = ref [] не дает полиморфностиa list ref тип.В противном случае вы можете использовать как int list и bool list, а также смешивать элементы разных типов, изменяя ссылку.Вместо этого он получает тип '_a list ref.Это означает, что тип не полиморфный, а просто unknown .Как только вы что-то делаете с a с определенным типом, он исправляет '_a раз и навсегда.

# let a = ref [];;
val a : '_a list ref = {contents = []}
# let sum_of_a = List.fold_left (+) 0 !a;;
val sum_of_a : int = 0
# a;;
- : int list ref = {contents = []}

Для более подробного объяснения ограничения значения и фактически примененного «ослабленного» ограничения значенияв контроллере типов OCaml см. статью Ослабление ограничения значения , автор Jacques Garrigue (2004).

Answer 2

В сообщении об ошибке от компилятора есть переменная слабого типа, но я не уверен, что слабая переменная связана с ошибкой (я не вижу, как состояние переменной типа могло быть причиной этого сообщения ).

Вы уверены, что не определяете два типа polynomial? Это вопрос чуть выше двух, указанных Гаше в его ответе в FAQ (« Сообщение об ошибке: тип не совместим с самим собой »).