Понимание ошибок ограничения значения F #

Question

Я не понимаю, как работает ограничение значения в F #. Я прочитал объяснение в вики , а также в документации MSDN . Что я не понимаю, так это:

1. Почему, например, это дает мне ошибку ограничения значения (взято из этого вопроса):

   let toleq (e:float<_>) a b = (abs ( a - b ) ) < e
   

   Но это не так:

   let toleq e (a:float<_>) b = (abs ( a - b ) ) < e
   

2. Это обобщенно все в порядке ...

   let is_bigger a b = a < b
   

   но это не так (указывается как int):

   let add a b = a + b
   

3. Почему функции с неявными параметрами генерируют ограничение значения:

   это:

   let item_count = List.fold (fun acc _ -> 1 + acc) 0
   

   против этого:

   let item_count l = List.fold (fun acc _ -> 1 + acc) 0 l
   

   (Имейте в виду, если я использую эту функцию во фрагменте кода, ошибка VR исчезнет, ​​но тогда будет указана функция того типа, для которого я ее использовал, и я хочу, чтобы она была обобщена)

Как это работает?

(я использую последнюю версию F #, v1.9.6.16)

Answer 1

EDIT

Более подробная / свежая информация здесь: Обобщение частично примененной функции

(оригинал ниже)

Я думаю, что прагматическая вещь здесь состоит не в том, чтобы попытаться понять это слишком глубоко, а в том, чтобы узнать пару общих стратегий, чтобы преодолеть виртуальную реальность и продолжить свою работу. Это немного «ответ», но я не уверен, что имеет смысл тратить время на понимание внутрикамерной системы типа F # (которая продолжает меняться незначительно от выпуска к выпуску) здесь.

Вот две основные стратегии, которые я бы отстаивал. Во-первых, если вы определяете значение с помощью типа функции (введите со стрелкой '->'), то убедитесь, что это синтаксическая функция, выполнив eta-translation :

// function that looks like a value, problem
let tupleList = List.map (fun x -> x,x)
// make it a syntactic function by adding argument to both sides
let tupleList l = List.map (fun x -> x,x) l

Во-вторых, если вы все еще сталкиваетесь с проблемами VR / обобщений, укажите полную сигнатуру типа, чтобы сказать, что вы хотите (а затем «отступите», как позволяет F #):

// below has a problem...
let toleq (e:float<_>) a b = (abs ( a - b ) ) < e
// so be fully explicit, get it working...
let toleq<[<Measure>]'u> (e:float<'u>) (a:float<'u>) (b:float<'u>) : bool = 
    (abs ( a - b ) ) < e
// then can experiment with removing annotations one-by-one...
let toleq<[<Measure>]'u> e (a:float<'u>) b = (abs ( a - b ) ) < e

Я думаю, что эти две стратегии - лучший прагматический совет. Тем не менее, вот моя попытка ответить на ваши конкретные вопросы.

1. Не знаю.

2. '>' - полностью универсальная функция ('a ->' a -> bool), которая работает для всех типов и, следовательно, is_bigger обобщает. С другой стороны, «+» - это встроенная функция, которая работает с несколькими примитивными типами и определенным классом других типов; он может быть обобщен только внутри других «встроенных» функций, в противном случае он должен быть привязан к определенному типу (или по умолчанию будет «int»). («Встроенный» метод специального полиморфизма - это то, как математические операторы в F # преодолевают отсутствие «классов типов».)

3. Это проблема «синтаксической функции», которую я обсуждал выше; «Давайте скомпилируем в поля / свойства, которые, в отличие от функций, не могут быть общими. Так что, если вы хотите, чтобы он был общим, сделайте его функцией. (См. Также этот вопрос для другого исключения из этого правила.)

Answer 2

Значение ограничения было введено для решения некоторых проблем с полиморфизмом при наличии побочных эффектов. F # наследует это от OCaml, и я считаю, что ограничение значения существует во всех вариантах ML. Вот вам несколько больше ссылок для чтения, кроме ссылок, которые вы цитировали. Поскольку Haskell является чистым, он не подвергается этому ограничению.

Что касается ваших вопросов, я думаю, что вопрос 3 действительно связан с ограничением стоимости, в то время как первые два - нет.

Answer 3

Никто, включая людей из команды F #, не знает ответа на этот вопрос каким-либо значимым образом.

Система логического вывода типа F # очень похожа на грамматику VB6 в том смысле, что компилятор определяет истину.

Прискорбно, но верно.