Странная GHCi ленивая оценка

Я определяю два взаимно-рекурсивных списка для четных и нечетных чисел в ghci следующим образом:

> let evens = 0:map (+1) odds; odds = map (+1) evens

И затем я обращаюсь к thunks, используя :sp

> :sp evens
evens = _
> :sp odds
odds = _
> take 5 evens
[0,2,4,6,8]
> :sp evens
evens = 0 : 2 : 4 : 6 : 8 : _
:sp odds
odds = _

Обратите внимание на то, что odds thunk не оценивается, хотя evens был оценен для 5-го элемента. Я могу представить себе интуитивное объяснение этого. odds должен быть явно вызван для оценки:

> take 5 odds
[1,3,5,7,9]
>:sp odds
odds = 1 : 3 : 5 : 7 : 9 : _

Однако теперь, когда я это делаю:

> take 10 evens
[0,2,4,6,8,10,12,14,16,18]
> :sp evens
evens = 0 : 2 : 4 : 6 : 8 : 10 : 12 : 14 : 16 : 18 : _
> :sp odds
odds = 1 : 3 : 5 : 7 : 9 : 11 : 13 : 15 : 17 : _

Обратите внимание, как теперь odds thunk оценивается всякий раз, когда evens оценивается? Почему odds не оценивался в первый раз и оценивался во второй раз и во всех последующих оценках? Что происходит?

Ответы

Ответ 1

Это связано с тем, как скомпилированы взаимно рекурсивные привязки с помощью GHC (и есть ли разница в том, имеют ли привязки явную подпись типа или нет).

Запишите следующую простую программу, которая предоставляет одну и ту же проблему, но устраняет все подозрения на роль, которую может играть целая перегрузка или ограничение мономорфизма:

module MutRec where

ft = False : map not tf
tf = map not ft

Загрузка этого в GHCi (я использую 7.6.3) дает:

*MutRec> take 5 ft
[False,False,False,False,False]
*MutRec> :sp ft
ft = False : False : False : False : False : _
*MutRec> :sp tf
tf = _

Посмотрите на код ядра для этого модуля

$ ghc -O0 MutRec -fforce-recomp -ddump-simpl -dsuppress-all
[1 of 1] Compiling MutRec           ( MutRec.hs, MutRec.o )

==================== Tidy Core ====================
Result size of Tidy Core = {terms: 28, types: 42, coercions: 0}

Rec {
ft1_rkA
ft1_rkA = : False a_rkC

tf1_rkB
tf1_rkB = map not ft1_rkA

a_rkC
a_rkC = map not tf1_rkB
end Rec }

ds_rkD
ds_rkD = (ft1_rkA, tf1_rkB)

ft
ft = case ds_rkD of _ { (ft2_Xkp, tf2_Xkr) -> ft2_Xkp }

tf
tf = case ds_rkD of _ { (ft2_Xkq, tf2_Xks) -> tf2_Xks }

Это все объясняет. Взаимосвязанные определения заканчиваются блоком Rec, ссылаясь друг на друга напрямую. Но тогда GHC создает пару ds_rkD и повторно извлекает компоненты из пары. Это дополнительное направление. Это объясняет, почему после частичной оценки ft в GHCi верхняя часть tf будет по-прежнему отображаться как удар, даже если под ней была оценка. На самом деле, мы можем проверить, что просто выполнить минимальную оценку на tf достаточно, чтобы разоблачить это:

*MutRec> take 5 ft
[False,False,False,False,False]
*MutRec> :sp ft
ft = False : False : False : False : False : _
*MutRec> :sp tf
tf = _
Prelude MutRec> seq tf ()
()
Prelude MutRec> :sp tf
tf = True : True : True : True : _

Если мы добавим синтаксис синтаксиса в ft и tf или включим оптимизацию, построение кортежа не произойдет:

$ ghc -O MutRec -fforce-recomp -ddump-simpl -dsuppress-all
[1 of 1] Compiling MutRec           ( MutRec.hs, MutRec.o )

==================== Tidy Core ====================
Result size of Tidy Core = {terms: 12, types: 11, coercions: 0}

Rec {
ft1
ft1 = map not tf

ft
ft = : False ft1

tf
tf = map not ft
end Rec }

Теперь GHCi будет вести себя более естественно.

Изменить

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

Если связывание является полиморфным, но не имеет сигнатуры типа, тогда оно рекурсивно использует мономорфный. Это ограничение в Hindley-Milner, которое GHC также реализует. Если ты хочешь полиморфной рекурсии, вам нужна дополнительная подпись типа.

Чтобы правильно сформулировать это на языке Core, desugarer делает мономорфную копию каждая неаннотированная рекурсивная функция. Эта мономорфная версия используется в рекурсивном вызовов, обобщенная версия используется для внешних вызовов. Вы можете видеть это даже для небольшого функции, такой как rep (что является повторной реализацией repeat). Ядро desugared для

rep x = x : rep x

является

rep
rep =
  \ (@ a_aeM) ->
    letrec {
      rep_aeJ
      rep_aeJ =
        \ (x_aeH :: a_aeM) -> : @ a_aeM x_aeH (rep_aeJ x_aeH); } in
    rep_aeJ

Внешний rep является полиморфным, а следовательно, абстракцией типа \ (@ a_aeM) -> в начале. Внутренний rep_aeJ является мономорфным и используется в рекурсивном вызове.

Если вы добавляете явную аннотацию типа к rep

rep :: a -> [a]
rep x = x : rep x

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

Rec {
rep
rep = \ (@ a_b) (x_aeH :: a_b) -> : @ a_b x_aeH (rep @ a_b x_aeH)
end Rec }

Вы можете увидеть, как тип аргумента @ a_b забирается в начале и повторно применяется до rep в каждом рекурсивном вызове.

Конструкция кортежа, которую мы видим для взаимно рекурсивных привязок, - это просто обобщение этого принципа. Вы создаете внутренние мономорфные версии взаимно рекурсивных функций, затем обобщают их в кортеже и извлекают полиморфные версии из кортежа.

Все это происходит независимо от того, являются ли привязки фактически полиморфными или нет. Достаточно для них быть рекурсивным. Я думаю, что это поведение GHC полностью правильно и нормально, в частности, потому что оптимизация позаботится об ударе производительности.