deniok: (Рыжий)
deniok ([personal profile] deniok) wrote2016-02-18 05:16 pm
Entry tags:

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

Между 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".

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

[identity profile] maxim.livejournal.com 2016-02-18 06:48 pm (UTC)(link)
Наиболишие и наименьшие — это коиндуктивные и индуктивные соответственно.
Это фикспойнты типов, они в нормальной форме нерекурсивно кодируются любые.
Edited 2016-02-18 18:49 (UTC)