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

Есть ли что-то принципиально иное в дизайне или идеологии 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 # не может выразить тип «некоторый класс с длиной член ".

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

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

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

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

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

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

Однако эти подходы, как правило, дают плохие сообщения об ошибках и плохие intellisense создает визуальный редактор "

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

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

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

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

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

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