Почему GHC выводит мономорфный тип здесь, даже с отключенным MonomorphismRestriction? - PullRequest
Новая
       36

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

16 голосов
/ 28 марта 2019

Это было вызвано Разрешением типа `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 Ответ

19 голосов
/ 28 марта 2019

Полиморфная рекурсия (когда функция вызывает себя с типом, отличным от того, для которого она была вызвана) всегда требует сигнатуры типа. Полное объяснение приведено в Раздел 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 на 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)
...