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:17 pm (UTC)(link)
система типов гарантирует нормальные формы, ну и отсутствие Fix аксиомы соответственно любых термов, базовая библиотека через foldr вся написана.
использование fix разрешено только как макро-расширение базового CoC языка (допустим).
Эта же штука (колбаса), что я привел это же в один фолд с деревом паттерн мачинга преображается, так как это хвостовая рекурсия. Т.е. что то типа, компилируем только хвостовые рекурсии — ограничение для такого macro-fix.
Edited 2016-02-18 18:40 (UTC)

[identity profile] deni-ok.livejournal.com 2016-02-18 06:41 pm (UTC)(link)
Такое могу написать
> let collatz = fix (\c n -> if n == 1 then 1 else if even n then c (n `div` 2) else c (3 * n + 1))

[identity profile] maxim.livejournal.com 2016-02-18 06:45 pm (UTC)(link)
хех, так тут параметр экспонента, а я например только про параметры полиномиальные функторы :-)

[identity profile] deni-ok.livejournal.com 2016-02-18 08:27 pm (UTC)(link)
А чем тогда терминировать fix, если он на уровне термов?
> :t fix ('z' :)
fix ('z' :) :: [Char]
> fix ('z' :)
"zzzzzzzzzzzzzzzzzzzInterrupted.

[identity profile] maxim.livejournal.com 2016-02-18 08:28 pm (UTC)(link)
так терминировать надо не фикс а индуктивные конструкции на которых он работает, это же обычный лямбда-терм. должен быть код с терминалами. Например из reverse/2 можно вывести, что первый параметр содержит терминал. А если задать типы так вообще никаких проблем.
Edited 2016-02-18 20:30 (UTC)