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

[deni_ok]

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

Comments

[maxim]

А есть какой-то алгоритм перевода Фикспойнт термов в правые фолды (с ограничениями)?
Я хочу примитивные фикспойнт потоковые парсеры (FSM) транслировать в foldr.
Типа в языке рекурсия чтобы присуствовала как понятие, но в ядре тайпчекера ее нет.

[deni_ok]

А зачем fix в языке, примитивной рекурсии над Nat недостаточно?

[maxim]

ну я вот про такую запись

expr([{N,X}|T],[{typevar,Y}|Acc]) -> expr(T,[{N,X},{typevar,Y}|Acc

[nponeccop]

Оно undecidable, но это ничего не значит

http://stackoverflow.com/a/14719346 - полезная ссылка про наименьшие и наибольшие фикспоинты

[maxim]

Наиболишие и наименьшие - это коиндуктивные и индуктивные соответственно.
Это фикспойнты типов, они в нормальной форме нерекурсивно кодируются любые.

[deni_ok]

Ну я же не знаю, (1) гарантирует ли твоя система типов сильную нормализуемость всех термов и (2) в каких контекстах разрешено использовать fix. В общем случае неразрешимо, конечно.

[maxim]

система типов гарантирует нормальные формы, ну и отсутствие Fix аксиомы соответственно любых термов, базовая библиотека через foldr вся написана.
использование fix разрешено только как макро-расширение базового CoC языка (допустим).
Эта же штука (колбаса), что я привел это же в один фолд с деревом паттерн мачинга преображается, так как это хвостовая рекурсия. Т.е. что то типа, компилируем только хвостовые рекурсии - ограничение для такого macro-fix.

[deni_ok]

Такое могу написать

> let collatz = fix (\c n -> if n == 1 then 1 else if even n then c (n `div` 2) else c (3 * n + 1))

[maxim]

хех, так тут параметр экспонента, а я например только про параметры полиномиальные функторы :-)

[deni_ok]

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

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

[maxim]

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