Что такое главный тип?

Ответ 1

Процесс вывода типа является фактом угадывания, исходя из написанной пользователем программы, типа этой программы. В общем, может быть несколько правильных типов для данной программы. Например, программе fun x → x можно дать типы int → int и bool → bool.

Для данной программы тип этой программы является основным, если это наиболее общий тип, который может быть задан этой программе, в том смысле, что все другие возможные типы являются специализацией (экземплярами) этого типа. С моим fun x → x примером fun x → x полиморфный 'a → 'a является основным типом.

В некоторых системах типов основные типы не всегда существуют. У вас есть программа P с двумя возможными типами T1 и T2, ни один из которых не является более общим, чем другой. Например, в некоторых системах, где числовые операторы перегружены, программе fun x → x + x может быть задан тип int → int и тип float → float, и нет типа, включающего оба. Это проблема для механизма вывода, поскольку это означает, что он должен сделать произвольный выбор, выбрать один из возможных типов, не зная, предназначен ли он для пользователя. Если у вас есть основные типы, процесс вывода не должен делать никакого выбора.

(Для решения этого примера вы могли бы: (1) не перегружать арифметические операторы (2) сделать произвольный выбор (то, что F # делает iirc) (3) отклонить программу и запросить аннотацию типа для удаления неоднозначности (4) иметь больше выразительные типы, такие как Haskell Num a => a → a.)

"Простое" подмножество языка OCaml, основанное на выводе типов Хиндли-Милнера, имеет основные типы. Это означает, что механизм логического вывода всегда делает правильные вещи (учитывая спецификацию возможных типов). Некоторые более продвинутые аспекты системы типов (например, полиморфные поля и методы) теряют это свойство: в некоторых случаях система типов не может найти наиболее общий тип, или для поиска наиболее общего типа потребуются значительно более сложные вычисления из механизм вывода типа (который обычно пытается быть быстрым). Опция -principal - это ручка, которая, если я правильно помню, будет:

• fail - это некоторый случай, когда средство проверки типов в противном случае приняло бы решение, не относящееся к -principal (сделало произвольный выбор)
• стараться найти основное решение за счет увеличения времени проверки типов и использования памяти

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

Еще две технические детали, если вы хотите пойти дальше:

• Понятие ML о "главных типах" - это вопрос о том, существует ли наиболее общий тип для данной среды фиксированного типа; некоторые авторы изучают вопрос о том, существует ли у них самая общая пара (среда, тип), так называемая "главная типизация"; это более сложный вопрос (вы должны вывести то, что вы ожидаете от других модулей, в то время как в ML вы получаете сигнатуры для внешних модулей, на которые вы полагаетесь; а выводить полиморфизм очень сложно), который не используется в большинстве программ, основанных на ML языки.

• Существование главных типов является тонким равновесием для разработчиков системы типов. Если вы удалите элементы из системы типов ML (полиморфизм, такие как 'a → 'a), вы потеряете принципальность, но если вы добавите силу (переходя от ML к System F, которая имеет более выразительные полиморфные типы), вы также можете потерять княжество. Вы можете восстановить утраченное княжество, перейдя к системам еще более сложного типа, таким как MLF, но это сложная проблема.

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

Ответ 2

Чтобы немного поразмышлять об объяснении газа, вот пример, украденный у OCaml собственными testuite, где появляется княжество или его отсутствие. Отказ от ответственности: здесь используются объекты.

class c = object method id : 'a. 'a -> 'a = fun x -> x end;;
type u = c option;;
let just = function None -> failwith "just" | Some x -> x;;
let f x = let l = [Some x; (None : u)] in (just(List.hd l))#id;;
let g x =
  let none = (fun y -> ignore [y;(None:u)]; y) None in
  let x = List.hd [Some x; none] in (just x)#id;;
let h x =
  let none = let y = None in ignore [y;(None:u)]; y in 
  let x = List.hd [Some x; none] in (just x)#id;;

При запуске этого сеанса верхнего уровня вы получите:

#     val f : c -> 'a -> 'a = <fun>
#     val g : c -> 'a -> 'a = <fun>
#     val h : < id : 'a; .. > -> 'a = <fun>

Эти функции выполняют то же самое, но назначаются разные типы!

Если вы вызываете OCaml с опцией -principal, запускаются первые два примера:

Warning 18: this use of a polymorphic method is not principal.

Интересно, что если вы замените 'a на тип h на 'a -> 'a, вы получите тот же тип, что и f и g, так как тип c - это просто тип сокращается (т.е. расширяется до) < id: 'a -> 'a; .. >.

Что компилятор хочет сказать программисту здесь, что существует два подходящих типа для f и g, и что нет критерия, который помог бы OCaml решить, какой из них является "лучшим" (и "лучший", я имею в виду, конечно же, принципал!).