[Haskell] callCC почему обрывается вычисление
От: achmed Удмуртия https://www.linkedin.com/in/nail-achmedzhanov-9907188/
Дата: 22.06.09 20:34
Оценка:
Добрый вечер!

Перечитал Haskell/Continuation passing style несколько раз,
но никак не пойму, почему при вызове k вычисление обрывается.

callCC $ \k -> do k 3
                  return 3


Как это происходит при такой "простой" реализации callCC?
callCC f = Cont $ \k -> runCont (f (\a -> Cont $ \_ -> k a)) k
Re: [Haskell] callCC почему обрывается вычисление
От: Mr.Cat  
Дата: 22.06.09 22:05
Оценка: 6 (1)
Здравствуйте, achmed, Вы писали:
A>но никак не пойму, почему при вызове k вычисление обрывается.
A>Как это происходит при такой "простой" реализации callCC?
A>
A>callCC f = Cont $ \k -> runCont (f (\a -> Cont $ \_ -> k a)) k
A>

Все дело в волшебных пузырь^W^W ленивости языка.
Смотри. Вот у нас есть бинд:
m >>= g = Cont (\k -> runCont m (\a -> runCont (g a) k))

Теперь представь, что m — это вызов захваченной с помощью call/cc континуации, т.е.
(\a -> Cont $ \_ -> k a) v

или попросту
Cont $ \_ -> k v

Очевидно, что в этом случае результат вычисления бинда не зависит от g, поэтому "(\a -> runCont (g a) k)" никогда не будет вычислен (язык-то ленивый), и "Cont $ \_ -> k v" станет результатом вызова f.

Как-то так.
Re: [Haskell] callCC почему обрывается вычисление
От: palm mute  
Дата: 23.06.09 07:18
Оценка: 4 (1)
Здравствуйте, achmed, Вы писали:

A>Добрый вечер!


A>Перечитал Haskell/Continuation passing style несколько раз,

A>но никак не пойму, почему при вызове k вычисление обрывается.

Отложим для начала монаду Cont в сторону, вспомним обычный CPS. Как программы в CPS "возвращают" результаты? Они передают их продолжениям как аргументы:
mul a b = \k -> k (a * b)
test_mul = mul 3 4 print


Что нужно сделать, чтобы "прервать" вычисление? Нет ничего проще, нужно проигнорировать продолжение:
cpsDiv a b k = if b == 0 then putStrLn "division by zero" else k (a `div` b)
test_div = do cpsDiv 10 5 print
              cpsDiv 3 0 print -- здесь вместо print вызовется putStrLn "division by zero" по очевидным причинам


Можно сказать, что монада Cont преобразует монадную программу в CPS. Вовзрат или невозврат в монаде Cont происходит точно так же, только продолжения передаются "за кулисами".
Если присмотреться (очень внимательно и вдумчиво присмотреться) к определению callCC, мы увидим, что внутреннее подвыражение (выделено курсивом) игнорирует "свое" продолжение, передавая результат в "чужое":

callCC f = Cont $ \k -> runCont (f (\a -> Cont $ \_ -> k a)) k


Напоследок замечу, что тип данных Cont — это всего лишь функция ((a->r)->r). Он нужен, т.к. только для новых типов данных можно объявлять свои instances (в данном случае — instance Monad).
Потому может быть полезно для понимания callCC убрать лишние заворачивания и разворачивания, нужные только тайп-чекеру Haskell, получив:
callCC f = \k -> f (\a -> \_ -> k a) k
Re[2]: [Haskell] callCC почему обрывается вычисление
От: palm mute  
Дата: 23.06.09 07:30
Оценка: 6 (1)
Здравствуйте, Mr.Cat, Вы писали:

MC>Все дело в волшебных пузырь^W^W ленивости языка.

MC>Смотри. Вот у нас есть бинд:
MC>
MC>m >>= g = Cont (\k -> runCont m (\a -> runCont (g a) k))
MC>

MC>...
MC>Очевидно, что в этом случае результат вычисления бинда не зависит от g, поэтому "(\a -> runCont (g a) k)" никогда не будет вычислен (язык-то ленивый), и "Cont $ \_ -> k v" станет результатом вызова f.

Все хорошо, только ленивость здесь ни при чем. g — функция, потому нам не нужна ленивость, чтобы она "не вычислилась", ее достаточно просто не вызывать.
Монаду Cont можно с успехом определить на строгом Ocaml:
let return x = fun k -> k x
let (>>=) m k = fun c -> m (fun a -> k a c)
let callCC f = fun k -> f (fun a _ -> k a) k

let rec product xs =
    callCC (fun exit ->
        match xs with
            []      ->  return  1
          | (x::xs) ->
            begin 
                print_int x;
                if x=0 then exit 0 else product xs >>= (fun r -> return (r * x))
            end)


let id x = x
let test = product [1;2;4;3;9] id
let test2 = product [1;2;3;4;5;0;11;12;13] id

Функция product при обнаружении нуля в списке мгновенно завершается.
Re[3]: [Haskell] callCC почему обрывается вычисление
От: Mr.Cat  
Дата: 23.06.09 07:51
Оценка:
Здравствуйте, palm mute, Вы писали:
PM>Все хорошо, только ленивость здесь ни при чем. g — функция, потому нам не нужна ленивость, чтобы она "не вычислилась", ее достаточно просто не вызывать.
Ммм, действительно . G спрятана под лямбду, так что просто не вызывается, если не вызывается эта самая лямбда.
Re[3]: [Haskell] callCC почему обрывается вычисление
От: achmed Удмуртия https://www.linkedin.com/in/nail-achmedzhanov-9907188/
Дата: 23.06.09 18:39
Оценка:
Здравствуйте, palm mute, Вы писали:

PM>Все хорошо, только ленивость здесь ни при чем. g — функция, потому нам не нужна ленивость, чтобы она "не вычислилась", ее достаточно просто не вызывать.

PM>Монаду Cont можно с успехом определить на строгом Ocaml:
PM> ...

Здорово . К сожалению в wiki как то неоднозначно изложен этот момент.

There are two possible execution routes: either the condition for the when succeeds, k doesn't use continuation providing by the inner do-block which finally takes the continuation which is argument of return Cont-value of the callCC, k uses directly the continuation which is argument of return Cont-value of the callCC, expressions inside do-block after k will totally not be used, because Haskell is lazy, unused expressions will not be executed. If the condition fails, the when returns return () which use the continuation providing by the inner do-block, so execution passes on.

Re[3]: [Haskell] callCC почему обрывается вычисление
От: achmed Удмуртия https://www.linkedin.com/in/nail-achmedzhanov-9907188/
Дата: 23.06.09 21:08
Оценка: 9 (1)
Здравствуйте, palm mute, Вы писали:

PM>Монаду Cont можно с успехом определить на строгом Ocaml:

PM>
PM>let return x = fun k -> k x
PM>let (>>=) m k = fun c -> m (fun a -> k a c)
PM>let callCC f = fun k -> f (fun a _ -> k a) k

PM>let rec product xs =
PM>    callCC (fun exit ->
PM>        match xs with
PM>            []      ->  return  1
PM>          | (x::xs) ->
PM>            begin 
PM>                print_int x;
PM>                if x=0 then exit 0 else product xs >>= (fun r -> return (r * x))
PM>            end)


PM>let id x = x
PM>let test = product [1;2;4;3;9] id
PM>let test2 = product [1;2;3;4;5;0;11;12;13] id
PM>

PM>Функция product при обнаружении нуля в списке мгновенно завершается.

Ради спортивного интереса тот же пример на F#
#light

open System


type ContBuilder() =
    member this.Return(x) = (fun k -> k x)
    member this.Bind(m,f) = (fun k -> m (fun a -> f a k))
let K = new ContBuilder()

let callCC f = fun k -> f (fun a _ -> k a) k
let id = fun x -> x
                     
let rec product2 xs = callCC (fun (exit) -> 
   K{
        match xs with
          | [] -> return 1
          | (h::t) -> 
            do print_any h
            if (h=0) then
                return! exit 0;
                else
                let! v = product2 t
                return v * h
    } )

let test = product2 [1;2;4;3;9] id
let test2 = product2 [1;2;3;4;5;0;11;12;13] id

printfn "test = %d" test 
printfn "test2 = %d" test2
Re[3]: [Haskell] callCC почему обрывается вычисление
От: BulatZiganshin  
Дата: 24.06.09 11:55
Оценка:
Здравствуйте, palm mute, Вы писали:

PM>Все хорошо, только ленивость здесь ни при чем. g — функция, потому нам не нужна ленивость, чтобы она "не вычислилась", ее достаточно просто не вызывать.

PM>Монаду Cont можно с успехом определить на строгом Ocaml:

уточню — ленивость это когда все значения являются функциями, "которые можно не вызывать". к примеру, возьмём f(x+1). на строгом языке сложение будет выполнено всегда, перед вызовом f. в ленивом языке сначала вызовется f, а сложение будет выполнено позже, только при необходимости получить численное значение этого параметра. однако если мы передадим в f нуль-арную функцию, вычисляющую то же значение, то сможем имитировать ленивость в строгом языке: f (fun: x+1)

преимущество хаскела только в том, что все его значения — ленивые, т.е. нам не нужно никакого синтаксического оверхеда для записи этой нуль-арной функции. в записи типа do f(x+1); g(y+1); h(z+1) все операции априори ленивые, тогда как в ML для достижения того же эффекта нам придётся писать более длинные выражения
Люди, я люблю вас! Будьте бдительны!!!
 
Подождите ...
Wait...
Пока на собственное сообщение не было ответов, его можно удалить.