Почему вывод типа F # настолько изменчив?

Question

Компилятор F #, по-видимому, выполняет вывод типов (довольно) строго сверху вниз, слева направо.Это означает, что вы должны делать такие вещи, как помещать все определения перед их использованием, порядок компиляции файлов значителен, и вам, как правило, нужно переставлять вещи (через |> или что у вас), чтобы избежать явных аннотаций типов.

Насколько сложно сделать это более гибким, и планируется ли это для будущей версии F #?Очевидно, что это можно сделать, так как, например, у Haskell нет таких ограничений с таким же мощным выводом.Есть ли что-то принципиально иное в дизайне или идеологии F #, что вызывает это?

Answer 1

Есть ли что-то принципиально иное в дизайне или идеологии F #, что является причиной этого?

Да. F # использует номинальную, а не структурную типизацию, потому что она проще и, следовательно, проще для простых смертных.

Рассмотрим пример F #:

let lengths (xss: _ [] []) = Array.map (fun xs -> xs.Length) xss

let lengths (xss: _ [] []) = xss |> Array.map (fun xs -> xs.Length)

Первый не компилируется, потому что тип xs внутри анонимной функции не может быть выведен, потому что F # не может выразить тип "некоторый класс с Length членом".

Напротив, OCaml может выражать прямой эквивалент:

let lengths xss = Array.map (fun xs -> xs#length) xss

потому что OCaml может выражать этот тип (он написан <length: 'a ..>). Обратите внимание, что это требует более мощного вывода типа, чем F # или Haskell в настоящее время, например. OCaml может определять типы сумм.

Однако эта функция, как известно, является проблемой удобства использования. Например, если вы напортачили в другом месте кода, то компилятор еще не определил, что тип xs должен быть массивом, поэтому любое сообщение об ошибке, которое он может выдать, может предоставить только информацию типа «некоторый тип с членом длины». а не "массив". Только с немного более сложным кодом это быстро выходит из-под контроля, поскольку у вас есть массивные типы со многими структурно выведенными элементами, которые не совсем объединяются, что приводит к непонятным (C ++ / STL-подобным) сообщениям об ошибках.

Answer 2

Что касается "столь же мощного вывода Хаскелла", я не думаю, что Хаскеллу приходится иметь дело с

• Динамический подтип в стиле OO (классы типов могут делать что-то похожее, но классы типов проще набирать / выводить)
• перегрузка метода (классы типов могут делать что-то подобное, но классы типов легче набирать / выводить)

То есть, я думаю, что F # имеет дело с некоторыми сложными вещами, которые Хаскелл не делает. (Почти наверняка Haskell имеет дело с некоторыми трудностями, которых нет у F #.)

Как отмечается в других ответах, большинство основных языков .NET имеют инструментальные средства Visual Studio в качестве основного влияния на разработку языка (см., Например, как LINQ имеет «from ... select» вместо SQL-y »select. .. from ", мотивированный получением intellisense из префикса программы). Интеллектуальность, загадочность ошибок и понятность сообщений об ошибках - все это факторы, определяющие дизайн F #.

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

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

Answer 3

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

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

Еще одна мысль об этом заключается в том, что проверка кода сверху вниз соответствует тому, как мы читаем код (по крайней мере, иногда). Таким образом, возможно тот факт, что мы склонны писать код таким образом, который делает возможным вывод типов, также делает код более читабельным для людей ...

Answer 4

F # использует однопроходную компиляцию, так что Вы можете ссылаться только на типы или функции, которые были определены либо ранее в файле вы в настоящее время или появляются в файле, который указан ранее в порядок компиляции.

Я недавно спросил Дона Сайма о несколько проходов источника для улучшения процесс вывода типа. Его ответ был «Да, можно сделать несколько проходов вывод типа. Это также вариации за один проход, которые генерируют конечный набор ограничений.

Однако эти подходы имеют тенденцию давать плохие сообщения об ошибках и плохие Intellisense приводит к визуальному редактор. "

http://www.markhneedham.com/blog/2009/05/02/f-stuff-i-get-confused-about/#comment-16153

Answer 5

Короткий ответ заключается в том, что F # основан на традициях SML и OCaml, тогда как Haskell происходит из несколько иного мира Миранды, Гофера и тому подобного.Различия в исторической традиции неуловимы, но широко распространены.Это различие параллельно и в других современных языках, таких как ML-подобный Coq, который имеет те же ограничения порядка, что и Haskell-подобный Agda, который не имеет.

Это различие связано с ленивым против строгой оценки.Сторона вселенной Haskell верит в лень, и как только вы уже поверите в лень, идея добавить лень к таким вещам, как вывод типа, не представляет никакой сложности.Принимая во внимание, что на стороне ML вселенной всякий раз, когда необходима лень или взаимная рекурсия, это должно быть явно отмечено использованием ключевых слов, таких как с , и , rec ,и т. д. Я предпочитаю подход на Haskell, потому что он приводит к меньшему количеству шаблонного кода, но есть много людей, которые думают, что лучше сделать эти вещи явными.