6.12.2. Обобщение let-связываний

MonoLocalBinds

Подразумевается расширением:

TypeFamilies, GADTs

Начиная с версии:

6.12.1

Статус:

Включено в GHC2024

По умолчанию выводятся менее полиморфные типы для локальных связываний.

В языке в стиле ML тип любой переменной, связанной с помощью let или where, обычно обобщается, чтобы быть максимально полиморфным. С расширением MonoLocalBinds GHC применяет несколько более консервативную политику по причинам, описанным в разделе 4.2 статьи OutsideIn(X): модульный вывод типов с локальными предположениями, а также в связанной записи в блоге.

Расширение MonoLocalBinds подразумевается расширениями TypeFamilies и GADTs. Его можно снова отключить с помощью NoMonoLocalBinds, но в этом случае вывод типов становится менее предсказуемым. (Прочитайте статью!)

В первом приближении при использовании MonoLocalBinds типы связываний верхнего уровня обобщаются, а типы локальных (то есть вложенных) связываний — нет. Идея состоит в том, что на верхнем уровне окружение типов не содержит свободных переменных типов, поэтому описанные в этих статьях трудности не возникают. Однако GHC применяет несколько более сложное правило, поскольку по стилистическим причинам программисты иногда пишут локальные связывания, не использующие локальные переменные, так что такие связывания могли бы находиться и на верхнем уровне. Кажется разумным обобщать их типы.

Итак, вот точные правила, используемые MonoLocalBinds. При включённом MonoLocalBinds группа связываний обобщается тогда и только тогда, когда выполняется одно из следующих условий:

• Это группа связываний верхнего уровня; или
• Каждая из её свободных переменных (за исключением переменных, связываемых самой группой) является замкнутой (см. следующий пункт); или
• Для одной из её связываемых переменных указана частичная сигнатура типа (см. раздел «Частичные сигнатуры типов»). Добавление частичной сигнатуры типа f :: _ (или, в более общем случае, f :: _ => _) позволяет для отдельного связывания попросить GHC выполнить let-обобщение, даже если включено MonoLocalBinds.

Даже если связывание обобщается, обобщение может не охватывать все его свободные переменные типов — либо потому, что оно упоминает локально связанные переменные, либо из-за Ограничения мономорфизма (Отчёт по Haskell, раздел 4.5.5).

Замкнутые переменные. Ключевая идея такова: если переменная замкнута, её тип определённо не содержит свободных переменных типов. Переменная f называется замкнутой тогда и только тогда, когда выполняется одно из следующих условий:

• Переменная f импортирована из другого модуля; или

• Переменная f связана с помощью let, и выполняется одно из следующих условий:

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

Обратите внимание, что сигнатура вида f :: a -> a эквивалентна f :: forall a. a -> a, если a не находится в области видимости. Следовательно, f является замкнутой, поскольку для неё указана полная сигнатура типа без свободных переменных.

Пример 1

g v = ...
    where
      f1 x = x+1
      f2 y = f1 (y*2)

У f1 есть свободная переменная (+), но она импортирована и, следовательно, замкнута. Поэтому связывание f1 обобщается. В результате её тип f1 :: forall a. Num a => a -> a не содержит свободных переменных типов, поэтому f1 является замкнутой. Следовательно, связывание f2 обобщается, поскольку обе её свободные переменные, f1 и (*), замкнуты.

Пример 2

f3 x = let g y = x+y in ....

У связывания g есть свободная переменная x, связанная лямбда-выражением, а потому не являющаяся замкнутой. Поэтому связывание g не обобщается.

Связывания верхнего уровня. Ограничение мономорфизма может привести к тому, что даже связывания верхнего уровня не будут обобщены, и, следовательно, даже окружение типов верхнего уровня может содержать свободные переменные типов. Тем не менее связывания верхнего уровня всегда обобщаются. Чтобы понять почему, рассмотрим

module M( f ) where
  x = 5
  f v = (v,x)

На связывание x=5 распространяется Ограничение мономорфизма, поэтому оно не обобщается, а значит, связывание f не является замкнутым. Если вследствие этого не обобщать f, мы в итоге экспортировали бы f :: Any -> (Any, Integer), при этом тип x был бы приведён к Integer, а тип v — к Any. Это противоречит интуиции и нежелательно, поэтому мы всегда обобщаем связывания верхнего уровня.