Recursive type for yielding function

This is the problem:

I have a function that yields a number N times. The caller invokes the function, and gets the number and a continuation. It does some work then invokes the continuation, getting another number and continuation. That repeats until N continuations are invoked.

Things become interesting when I try to type the continuation returned by the yielding function. It seems that it has a recursive type. Is that a known result? How do type systems deal with recursive types?

def numbers = fun(... -> return(Yield_int, int), throw(Exception) {...})
type Yield_int = fun(-> (Yield_int, int), (Exception))

I use continuation-passing style notation. Whatever comes after "->" is a continuation passed as argument to the function. By default a function takes two continuations, one for normal return and one for exceptions. So the notation above means the return value of Yield_int is the pair (Yield_int, int).

I am not sure how to manage the stack with a yielding function too. The Yield_int continuation looks like a capturing lambda, so I could allocate memory to hold captured variables. But I may need to allocate more memory for each Yield_int continuation, which does not look optimal.

My ideas range from a fragmented stack frame to read-only memory pages for the Yield_int continuation when it is not activated. That may not be a discussion for ltu...

Recursive datatype + delimited continuations

You can just put the (delimited) continuation in a recursive datatype that you return, like the following OCaml definition.

type 't yielding = More of ('t * (unit -> 't yielding))
                 | End

For example, here's a function of type int -> int yielding

let count_up_to n =
    let rec count_from i () =
        if (i <= n) then
            More (i, count_from (i + 1))
        else
            End
    in
        count_from 0 ()

Note that the "continuations" we're returning are really delimited continuations, because they capture the state of just part of the program (the rest of the execution of the count_up_to function), and may return a result. If you have a function for which it's inconvenient to write the delimited continuations explicitly like I did above, you could use a library providing the shift/reset or control/prompt operations to capture and return the delimited continuation.

By Sameer Sundresh at Sun, 2009-10-11 23:35 | login or register to post comments

You need a more general notion of continuation.

That's just a call-by-name list, which is a rather impoverished notion of a continuation. Every discussion of yield that I've seen relied on a more general notion of continuation.

The original post is a little light on details; and I'm not particularly familiar with the notation being used. However it does very much sound similar to something one of my friends has done; I developed a refunctionalized variant of his idea here

This code doesn't use "yield", although it could be rewritten to do so. My friend's yield uses a lazy list instead of the newtype Iterator, and of course a lazy list is a recursive datatype.

By Leon P Smith at Mon, 2009-10-12 01:28 | login or register to post comments

I agree that was a trivial

I agree that was a trivial example. As I mentioned, in the general case you could capture a delimited continuation and store it in the ('t yield) value returned. The implementation mechanism seems to be essentially what Denis needs. If you don't mind making the continuations returned by the yielding function use-once (e.g., give them a linear type), then you can cut some corners in the implementation by directly using the stack associated with the continuation rather than copying it to be safe.

By Sameer Sundresh at Wed, 2009-10-14 00:33 | login or register to post comments

Recursive datatype = OK

Thanks, that looks exactly what I want to do. I see that OCaml has no trouble with the recursive datatype, so it shouldn't be an issue for me either (?).

Even though I am using CPS I want to keep the continuation type away from programmer's hands as much as possible, so there will be a formalism that represents this specific use in dodo (using the notion of non-escaping labels).

Leon, my knowledge of Haskell is too limited to make much sense of your code but I see that the Iterator type is similarly recursive, which is a way I could have done it-- but I am more interested in the continuation approach.

By Denis Bredelet -jido at Mon, 2009-10-12 07:08 | login or register to post comments

Re: Recursive datatype = OK

My approach uses continuations, specifically from Control.Monad.Cont. :-) Actually the Iterator itself seems to me to be a kind of continuation, but it's not clear to me how to make it a monad, other than make it the result of the traditional continuation type.

I'm not sure how appropriate the name "Iterator" really is, but it corresponds to what my friend called an Iterator. In this case, the iterator mediates the communication between a process and the scheduler: when a process calls the scheduler, the process passes its current continuation as a "Iterator", and vice-versa.

The first half of the code defines a monad that allows a static number of concurrent processes that share a single global variable. The only scheduler provided is fairly brain-dead, and cannot make scheduling decisions on it's own. The second half doesn't make explicit use of continuations, and demonstrates a particular kind of race condition.

By Leon P Smith at Mon, 2009-10-12 16:05 | login or register to post comments

Lambda the Ultimate

User login

Navigation