deniok: (Рыжий)
[personal profile] 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".

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

Date: 2016-02-18 03:44 pm (UTC)
From: [identity profile] maxim.livejournal.com
А есть какой-то алгоритм перевода Фикспойнт термов в правые фолды (с ограничениями)?
Я хочу примитивные фикспойнт потоковые парсеры (FSM) транслировать в foldr.
Типа в языке рекурсия чтобы присуствовала как понятие, но в ядре тайпчекера ее нет.
Edited Date: 2016-02-18 04:11 pm (UTC)

Date: 2016-02-18 04:39 pm (UTC)
From: [identity profile] deni-ok.livejournal.com
А зачем fix в языке, примитивной рекурсии над Nat недостаточно?

Date: 2016-02-18 04:53 pm (UTC)
From: [identity profile] 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?
Edited Date: 2016-02-18 05:49 pm (UTC)

Date: 2016-02-18 05:58 pm (UTC)
From: [identity profile] nponeccop.livejournal.com
Оно undecidable, но это ничего не значит

http://stackoverflow.com/a/14719346 - полезная ссылка про наименьшие и наибольшие фикспоинты
Edited Date: 2016-02-18 06:12 pm (UTC)

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

Date: 2016-02-18 06:14 pm (UTC)
From: [identity profile] deni-ok.livejournal.com
Ну я же не знаю, (1) гарантирует ли твоя система типов сильную нормализуемость всех термов и (2) в каких контекстах разрешено использовать fix. В общем случае неразрешимо, конечно.

Date: 2016-02-18 06:17 pm (UTC)
From: [identity profile] maxim.livejournal.com
система типов гарантирует нормальные формы, ну и отсутствие Fix аксиомы соответственно любых термов, базовая библиотека через foldr вся написана.
использование fix разрешено только как макро-расширение базового CoC языка (допустим).
Эта же штука (колбаса), что я привел это же в один фолд с деревом паттерн мачинга преображается, так как это хвостовая рекурсия. Т.е. что то типа, компилируем только хвостовые рекурсии — ограничение для такого macro-fix.
Edited Date: 2016-02-18 06:40 pm (UTC)

Date: 2016-02-18 06:41 pm (UTC)
From: [identity profile] 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))

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

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

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

Date: 2016-02-19 01:37 am (UTC)
From: [identity profile] papa-lyosha.livejournal.com
Класс!

Profile

deniok: (Default)
deniok

April 2017

S M T W T F S
      1
23 45678
9101112131415
16171819202122
23242526272829
30      

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags
Page generated Sep. 24th, 2017 03:04 am
Powered by Dreamwidth Studios