Можем ли мы иметь переменные типа в позиции конструктора в системе типов Хиндли Милнера?

Важно то, образуют ли конструкторы типов язык терминов первого порядка (без редукционного поведения выражений конструкторов типов) или язык более высокого порядка (с лямбдами или аналогичными конструкциями на уровне типа).

В первом случае ограничения, возникающие из Fix, всегда универсальны в самом общем виде (при условии, что мы придерживаемся HM). В каждом c a b ~ t уравнении t должен быть преобразован в выражение приложения конкретного типа с той же формой, что и c a b, поскольку c a b не может быть преобразован в какое-либо другое выражение. Параметры более высокого порядка не являются проблемой, поскольку они тоже просто статичны, например, c [] ~ c f решается f = [].

В последнем случае c a b ~ t может или не может быть разрешимым. В некоторых случаях это решает c = \a b -> t, в других случаях нет универсального унификатора.

Высшие виды выходят за рамки базовой системы типов Хиндли-Милнера, но с ними можно обращаться таким же образом.

Грубо говоря, HM анализирует синтаксическое дерево выражения, связывает переменную свободного типа с каждым подвыражением и генерирует набор эквациональных ограничений для терминов типов, включающих переменные типа, в соответствии с правилами типизации. То же самое можно сделать и с высшими видами.

Затем ограничения решаются путем унификации. Типичный шаг в алгоритме объединения (далее псевдохаскелл)

(F t1 ... tn := G s1 ... sk) =
  | n/=k || F/=G  -> fail
  | otherwise     -> { t1 := s1 , ... , tn := sn }

(Обратите внимание, что это только часть алгоритма унификации.)

Выше F, G - символы конструктора типов, а не переменные. В унификации более высокого порядка нам нужно учитывать, что _4 _, _ 5_ также являются переменными. Мы могли бы попробовать следующее правило:

(f t1 ... tn := g s1 ... sk) =
  | n/=k          -> fail
  | otherwise     -> { f := g , t1 := s1 , ... , tn := sn }

Но ждать! Вышеупомянутое неверно, поскольку, например, f Int ~ Either Bool Int должен унифицироваться, когда f ~ Either Bool. Итак, нам нужно также рассмотреть случай, когда n/=k. В общем, простой набор правил

(f t := g s) =
  { f := g , t := s }
(F := G) =      -- rule for atomic terms
  | F /= G    -> fail
  | otherwise -> {}

(Опять же, это только часть алгоритма объединения. Другие случаи также должны быть обработаны, как указывает Андреас Россберг ниже.)