Рекурсивная взаимность

[deniok]

Между Haskell Report и GHC base имеется дивная взаимная рекурсия.

В GHC base мы имеем такое определение наименьшей неподвижной точки (least fixpoint)

fix :: (a -> a) -> a
fix f = let x = f x in x

В Haskell Report в разделе 3.12 описана трансляция для выражения let в ядро (привожу только релевантные правила)

...
let p = e1 in e0    =    case e1 of ˜p -> e0
                             where no variable in p appears free in e1
let p = e1 in e0    =    let p = fix (\˜p -> e1) in e0

с замечанием "where fix is the least fixpoint operator".

Чтобы понять рекурсию, нужно понять рекурсию.

Comments

[deni-ok.livejournal.com]

А чем тогда терминировать fix, если он на уровне термов?

> :t fix ('z' :)
fix ('z' :) :: [Char]
> fix ('z' :)
"zzzzzzzzzzzzzzzzzzzInterrupted.

[maxim.livejournal.com]

так терминировать надо не фикс а индуктивные конструкции на которых он работает, это же обычный лямбда-терм. должен быть код с терминалами. Например из reverse/2 можно вывести, что первый параметр содержит терминал. А если задать типы так вообще никаких проблем.