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, которая связана lambda-выражением, и поэтому не закрыта. Следовательно, связывание g не обобщается.

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

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

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