Почему GHC выводит мономорфный тип здесь, даже с отключенным ограничением Monomorphism?

Это было вызвано разрешением типа 'f = f (<*>) pure', в котором обсуждается более сложный пример, но этот тоже работает.

Следующее определение компилируется без проблем:

w :: Integral a => a
w = fromInteger w

... Конечно, это не работает во время выполнения, но это помимо вопроса. Дело в том, что само определение w использует специализированную версию w :: Integer. Понятно, что это подходящая реализация, и, следовательно, проверки типов.

Однако, если мы удалим подпись, то GHC выведет не вышеуказанный тип, а только конкретный:

w' = fromInteger w'

GHCi> :t w
w :: Integral a => a
GHCi> :t w'
w' :: Integer

Ну, когда я увидел это, я был совершенно уверен, что это ограничение мономорфизма на работе. Хорошо известно, что, например,

i = 3

GHCi> :t i
i :: Integer

хотя i :: Num p => p было бы вполне возможно. И действительно, i :: Num p => p выводится, если -XNoMonomorphismRestriction активен, т.е. если ограничение мономорфизма отключено.

Однако в случае w' выводится только тип Integer даже когда ограничение мономорфизма отключено.

Чтобы подсчитать, что это как-то связано с дефолтом:

fromFloat :: RealFrac a => Float -> a
q :: RealFrac a => a
q = fromFloat q
q' = fromFloat q'

GHCi> :t q
q :: RealFrac a => a
GHCi> :t q'
q' :: Float

Почему полиморфный тип не выводится?

Ответ 1

Полиморфная рекурсия (когда функция вызывает себя с типом, отличным от того, у которого она была вызвана) всегда требует сигнатуры типа. Полное объяснение приведено в разделе 4.4.1 отчета Haskell 2010:

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

Позже в этом же разделе представлен пример полиморфной рекурсии, поддерживаемой сигнатурой типа.

Насколько я понимаю, вывод без помощи типа обычно неразрешим при наличии полиморфной рекурсии, поэтому Хаскелл даже не пытается.

В этом случае проверка типов начинается с

w :: a

где a является мета-переменной. Поскольку fromInteger вызывается с w в качестве аргумента в своем собственном объявлении (и, следовательно, в своей группе объявлений), средство проверки типов объединяет a с Integer. Не осталось переменных для обобщения.

Небольшая модификация вашей программы дает другой результат по той же причине:

v = fromIntegral v

Исходя из ваших первоначальных рассуждений, Haskell выведет v :: forall a. Num a => a v :: forall a. Num a => a, по умолчанию v на RHS набирает Integer:

v :: forall a. Num a => a
v = fromIntegral (v :: Integer)

Но вместо этого он начинается с v :: a. Поскольку v передается fromIntegral, оно налагает Integral a. Наконец, он обобщает. a В итоге программа оказывается

v :: forall a. Integral a => a
v = fromIntegral (v :: a)