NoMonomorphismRestriction помогает сохранить совместное использование?

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

В 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)

Почему?

Ugh... Когда скомпилирован с оптимизацией, он быстр даже с ограничением мономорфизма.

Ответ 1

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

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

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

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

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

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

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 a 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')

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

Ответ 2

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

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

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

Учтите, что вы обманываете все это, чтобы в эти дни стрелять, чтобы не обобщать и т.д.