NoMonomorphismRestriction помогает сохранить общий доступ?

Question

Я пытался ответить на другой вопрос о полиморфизме против совместного использования, когда наткнулся на это странное поведение.

В GHCi, когда я явно определяю полиморфную константу, он не получает никакого совместного использования, что понятно:

> let fib :: Num a => [a]; fib = 1 : 1 : zipWith (+) fib (tail fib)
> fib !! 30
1346269
(5.63 secs, 604992600 bytes)

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

> :set -XNoMonomorphismRestriction
> let fib = 1 : 1 : zipWith (+) fib (tail fib)
> :t fib
fib :: Num a => [a]
> fib !! 50
20365011074
(0.00 secs, 2110136 bytes)

Зачем?!

Тьфу... Когда компилируется с оптимизацией, это быстро, даже если ограничение мономорфизма отключено.

Answer 1

Предоставляя явную сигнатуру типа, вы не позволяете GHC делать определенные предположения относительно вашего кода. Я покажу пример (взят из этого вопроса):

foo (x:y:_) = x == y
foo [_]     = foo []
foo []      = False

Согласно GHCi, тип этой функции Eq a => [a] -> Bool, как и следовало ожидать. Однако, если вы объявите foo с этой подписью вы получите ошибку "переменная неоднозначного типа".

Причина, по которой эта функция работает только без сигнатуры типа, заключается в том, что проверка типов работает в GHC. Когда вы опускаете сигнатуру типа, foo предполагается, что имеет монотип [a] -> Bool для некоторого фиксированного типа a, Когда вы закончите вводить группу связывания, вы обобщите типы. Вот где вы получаете forall a. ...,

С другой стороны, когда вы объявляете полиморфную сигнатуру типа, вы явно заявляете, что foo является полиморфным (и, следовательно, тип [] не должен соответствовать типу первого аргумента) и boom, вы получите неоднозначную переменную типа.

Теперь, зная это, давайте сравним ядро:

fib = 0:1:zipWith (+) fib (tail fib)
-----
fib :: forall a. Num a => [a]
[GblId, Arity=1]
fib =
  \ (@ a) ($dNum :: Num a) ->
    letrec {
      fib1 [Occ=LoopBreaker] :: [a]
      [LclId]
      fib1 =
        break<3>()
        : @ a
          (fromInteger @ a $dNum (__integer 0))
          (break<2>()
           : @ a
             (fromInteger @ a $dNum (__integer 1))
             (break<1>()
              zipWith
                @ a @ a @ a (+ @ a $dNum) fib1 (break<0>() tail @ a fib1))); } in
    fib1

И для второго:

fib :: Num a => [a]
fib = 0:1:zipWith (+) fib (tail fib)
-----
Rec {
fib [Occ=LoopBreaker] :: forall a. Num a => [a]
[GblId, Arity=1]
fib =
  \ (@ a) ($dNum :: Num a) ->
    break<3>()
    : @ a
      (fromInteger @ a $dNum (__integer 0))
      (break<2>()
       : @ a
         (fromInteger @ a $dNum (__integer 1))
         (break<1>()
          zipWith
            @ a
            @ a
            @ a
            (+ @ a $dNum)
            (fib @ a $dNum)
            (break<0>() tail @ a (fib @ a $dNum))))
end Rec }

С явной подписью типа, как с foo выше, GHC должен лечить fib как потенциально полиморфно-рекурсивное значение. Мы могли бы передать несколько разных Num словарь для fib в zipWith (+) fib ... и на этом этапе нам придется выбросить большую часть списка, так как разные Num означает разные (+), Конечно, после компиляции с оптимизацией GHC замечает, что Num словарь никогда не изменяется во время "рекурсивных вызовов" и оптимизирует его.

В ядре выше, вы можете увидеть, что GHC действительно дает fib Num словарь $dNum) опять и опять.

Так как fib без сигнатуры типа считалось мономорфным до завершения обобщения всей связывающей группы, fib части были даны точно такого же типа, как весь fib, Благодаря этому, fib похоже:

{-# LANGUAGE ScopedTypeVariables #-}
fib :: forall a. Num a => [a]
fib = fib'
  where
    fib' :: [a]
    fib' = 0:1:zipWith (+) fib' (tail fib')

А поскольку тип остается фиксированным, вы можете использовать только один словарь, указанный при запуске.

Answer 2

Здесь вы используете fib с одинаковым аргументом типа в обоих случаях, и GHC достаточно умен, чтобы увидеть это и выполнить совместное использование.

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

Попробуйте использовать термин x = 2 + 2 полиморфно в двух контекстах без ограничения мономорфизма, где в одном контексте вы show (div x 2) а в другом ты используешь show (x / 2), В одной настройке вы получите Integral а также Show ограничения, которые заставляют вас по умолчанию Integerв другой ты получаешь Fractional и Show ограничение и по умолчанию вы Doubleтаким образом, результат вычисления не передается, так как вы работаете с полиморфным термином, примененным к двум различным типам. С включенным ограничением мономорфизма, он пытается один раз установить значение по умолчанию для чего-то как интегрального, так и дробного и завершается неудачно.

Имейте в виду, его хитрость, чтобы заставить все это сгореть в эти дни, пусть не обобщая, и т.д.