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

[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 в языке, примитивной рекурсии над Nat недостаточно?

[maxim.livejournal.com]

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

expr([{N,X}|T],[{typevar,Y}|Acc])   -> expr(T,[{N,X},{typevar,Y}|Acc]);
expr([{N,X}|T],[{C,Y}|Acc])         -> expr(T,[{app,{{C,Y},{N,X}}}|Acc]);
expr([],           Acc) -> rewind(Acc,[],[]);
expr([close   |T], Acc) -> {T1,Acc1} = rewind(Acc,T,[]), expr(T1,Acc1);
expr([open    |T], Acc) -> expr(T,[{open}|Acc]);
expr([star    |T], Acc) -> expr(T,[{const,func(star)}|Acc]);
expr([arrow   |T], Acc) -> expr(T,[{arrow}|Acc]);
expr([lambda  |T], Acc) -> expr(T,[{lambda}|Acc]);
expr([pi      |T], Acc) -> expr(T,[{pi}|Acc]);
expr([colon   |T], Acc) -> expr(T,[{colon}|Acc]);
expr([{var,L},colon|T],Acc) -> expr(T,[{typevar,L}|Acc]);
expr([{remote,L}|T],   Acc) -> expr(T,[om:type(L)|Acc]);
expr([{var,L}|T],      Acc) -> expr(T,[{var,L}|Acc]).

rewind([{F}|Acc],         T, [{"→",{{app,{{typevar,{L,_}},{A,X}}},{B,Y}}}|R]) when F == lambda; F== pi
                                        -> rewind(Acc,T,[{{func(F),L},{{A,X},{B,Y}}}|R]);
rewind([{A,X}|Acc],       T, [{B,Y}|R]) -> rewind(Acc,T,[{app,{{A,X},{B,Y}}}|R]);
rewind([{A,X}|Acc],       T, R)         -> rewind(Acc,T,[{A,X}|R]);
rewind([{arrow},Y|Acc],   T, [X|R])     -> rewind(Acc,T,[{func(arrow),{Y,X}}|R]);
rewind([{open},{A,X}|Acc],T, [{B,Y}|R]) -> {T,om:flat([{app,{{A,X},{B,Y}}}|[R|Acc]])};
rewind([{open}|Acc],      T, R)         -> {T,om:flat([R|Acc])};
rewind([{colon}|Acc],     T, R)         -> {T,om:flat([R|Acc])};
rewind([],                T, R)         -> {T,R}.

Хочется потоковые парсеры через Fixpoint и Pattern Matching записывать (HOPE), а не как вереницу case.
И в тоже время, чтобы это все компилировалось в foldr.

Или это undecidable?

[nponeccop.livejournal.com]

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

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

[maxim.livejournal.com]

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

[deni-ok.livejournal.com]

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

[maxim.livejournal.com]

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

[deni-ok.livejournal.com]

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

> 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.livejournal.com]

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

[deni-ok.livejournal.com]

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

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

[maxim.livejournal.com]

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