Do Be Do Be Do

Monads and algebraic effects are general concepts that give a definition of what a "side-effect" can be: an instance of monad, or an instance of algebraic effect, is a specific realization of a side-effect. While most programming languages provide a fixed family of built-in side-effects, monads or algebraic effects give a structured way to introduce a new notion of effect as a library.

A recent avenue of programming language research is how to locally define several realizations of the same effect interface/signature. There may be several valid notions of "state" or "non-determinism" or "probabilistic choice", and different parts of a program may not require the same realization of those -- a typical use-case would be mocking an interaction with the outside world, for example. Can we let users locally define a new interpretation of an effect, or write code that is generic over the specific interpretation? There are several existing approaches, such as monad transformer stacks, free monads interpreters, monad reification and, lately, effect handlers, as proposed in the programming language Eff.

Frank, presented in the publication below, is a new language with user-defined effects that makes effect handling a natural part of basic functional programming, instead of a separate, advanced feature. It is a significant advance in language design, simplifying effectful programming. Functions, called operators, do not just start computing a result from the value of their arguments, they interact with the computation of those arguments by having the opportunity to handle any side-effects arising during their evaluation. It feels like a new programming style, a new calling convention that blends call-by-value and effect handling -- Sam Lindley suggested the name call-by-handling.

Frank also proposes a new type-and-effect system that corresponds to this new programming style. Operators handle some of the effects raised by their arguments, and silently forward the rest to the computation context; their argument types indicate which effects they handle. In other words, the static information carried by an argument types is the delta/increment between the effects permitted by the ambient computation and the effects of evaluating this argument. Frank calls this an adjustment over the ambient ability. This delta/increment style results in lightweight types for operators that can be used in different contexts (a form of effect polymorphism) without explicit quantification over effect variables. This design takes part in a research conversation on how to make type-and-effect systems usable, which is the major roadblock for their wider adoption -- Koka and Links are also promising in that regard, and had to explore elaborate conventions to elide their polymorphic variables.

Another important part of Frank's type-system design is the explicit separation between values that are and computations that do. Theoretical works have long made this distinction (for example with Call-By-Push-Value), but programmers are offered the dichotomy of either having only effectful expressions or expressing all computations as values (Haskell's indirect style). Frank puts that distinction in the hands of the user -- this is different from distinguishing pure from impure computations, as done in F* or WhyML.

If you wish to play with the language, a prototype implementation is available.


Do Be Do Be Do (arXiv)
Sam Lindley, Conor McBride, Craig McLaughlin
2017

We explore the design and implementation of Frank, a strict functional programming language with a bidirectional effect type system designed from the ground up around a novel variant of Plotkin and Pretnar’s effect handler abstraction.

Effect handlers provide an abstraction for modular effectful programming: a handler acts as an interpreter for a collection of commands whose interfaces are statically tracked by the type system. However, Frank eliminates the need for an additional effect handling construct by generalising the basic mechanism of functional abstraction itself. A function is simply the special case of a Frank operator that interprets no commands. Moreover, Frank’s operators can be multihandlers which simultaneously interpret commands from several sources at once, without disturbing the direct style of functional programming with values.

Effect typing in Frank employs a novel form of effect polymorphism which avoid mentioning effect variables in source code. This is achieved by propagating an ambient ability inwards, rather than accumulating unions of potential effects outwards.

We introduce Frank by example, and then give a formal account of the Frank type system and its semantics. We introduce Core Frank by elaborating Frank operators into functions, case expressions, and unary handlers, and then give a sound small-step operational semantics for Core Frank.

Programming with effects and handlers is in its infancy. We contribute an exploration of future possibilities, particularly in combination with other forms of rich type system.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Frank is not Frink?

There may be potential for name confusion with the existing language Frink.

Or is this yet another language/library inspired by Frink but with a slightly different name (e.g. Frinj (implemented in Clojure), Frins (implemented in Scala), Farnsworth (implemented in Perl), Halculon (implemented in Haskell) or Rink (implemented in Rust) ?)

Bonus points for the reader for knowing why Halculon and Farnsworth are tangentially related names. :)

Awesome paper

Thank you gashce for posting this. I've been mulling it over for the last few days. Their presentation of algebraic effects is very slick. This is nice work.

I'm still meaning to better understand the relationship between algebraic effects and the notion of processes that I've sketched in the past. The simple answer is that algebraic effects are a discipline of always answering each environment invocation with a single value response (as opposed to a more general back and forth exchange). This shallow encoding of effects into processes would seem to mean that processes are at least as powerful as algebraic effects, and so I wonder what the reverse encoding would look like.

For example, let's suppose you have an IO effect that has {open: String -> Handle, write: Handle -> String -> Unit, close: Handle -> ()}. Suppose you want to add logging to those operations. I guess you can make them return a suspended computation {open: { String -> [Logging] Handle}, ... }? This doesn't allow for continued back and forth, though. You must decide what all of the logging will be on the basis of a single interaction with the file system (so maybe a better example would have been a raw Filesystem effect that is used to handle IO). Also you might need double nullary application (foo!!) which my intuition says will be error prone for programmers.

A more general approach is to adopt a convention of never using effect constructors directly. Instead, you can use operations like {open': String -> [IO, Logging]Handle, ...}. These helper operations can hide the back and forth that you might want between the different effects and should be able to encode general process interactions. If you take this approach, though, it seems like most of the beauty of code like this is lost:

state : S -> <State S>X -> X
state _ x = x
state s <get -> k> = state s (k s)
state _ <put s -> k> = state s (k unit)

Edit: There are two separate issues. You can still write handlers like this if you don't need effects from effects, but some of the beauty of the substituional theory is lost if you don't use get & put directly in the client code. The other issue is that if you have to manually encode the back & forth with effects, that looks like it will be much messier. I'm very interested in hearing about a more idiomatic approach to this kind of thing with effects if one exists.

Most of the other questions I had look like they're addressed in the future work section, with the exception of this: the paper emphasizes that Frank doesn't support effect inference, but seems to leave open that Frank might support type inference. And yet type signatures and effect signatures seem to be fairly entangled in this scheme. I wonder if there's any way to annotate only the effects while leaving the types inferred?

Excellent questions

The syntax of Frank proposed in the paper actually restricts effectful operations (such as open, write in your example above) to a "pure" interface (A1 -> ... -> An -> B) instead of an arbitrary computation type (<Delta1>A1 -> ... -> <Deltan>An -> [Sigma]B). So your proposed (String -> [Logging]Handle) is not supported for now: catching an operation always gives a value, and handling it cannot add new effects to the ambient ability. (I asked the authors, and) Extending this is future work.

Note that the handlers of <IO> do not have to return the same type as what the operations return, this type only informs what handlers need to pass to the continuation. So you can write

logging_FS : <IO>X -> [Logging]X

or even more flexible forms such as

logging_FS : <IO>X -> LogState -> (LogState * X)

which lets you pass around an intermediate LogState value that contains aggregated information on how to log -- solving the "you must decide logging one IO operation at a time" problem you mentioned. This is, of course, just a state monad, so you can also do

logging_FS : <IO>X -> [LogState]X

and latter write a <LogState> handler that keeps its state and makes [Logging] decisions.

Thanks

Yes, I see that you can always pass the logging "up" from the handler by having it introduce the logging effect, but I was focusing on the case where you want to pass the logging effects back "down" into the continuation, giving it a chance to handle them. I should have made that explicit.

So really, they're the same thing

So once the authors extend interfaces to allow arbitrary computation types, there really won't be much difference between a process and effectful computation. The effectful approach just singles out one of the ports (yield pure value) and gives it special significance. In the process approach you do the same thing, but in the core calculus "yield" is just another port. I think I may have figured this out last time we discussed algebraic effects on here...

Hm

I don't have as much experience programming with processes (I'm sure Sam Lindley, who also works on Session Types, would have interesting things to say there), so I can't comment much besides agreeing that Frank's handling style feels a lot like message-passing to me.

There is a subtlety though: yield does not just put a value on a "preferred" channel, it also stops the computation -- yielding has no continuation. You can express that by turning any X value in a [Return X]0 computation, with (Return X := return : X -> 0), but are X and not-not-X really the same thing? We already know that intuitionistic logic can be generalized into classical logic by moving from "a value is returned" to "one of the output ports may be called", yet there remain relatively fundamental differences between the two -- for example we don't really know how to have a graceful dependent type theory for classical logic.

I would thus say that I don't understand the difference enough to tell whether this is just a question of style (one presentation being more familiar than the other to some audience, or maybe more convenient to program in the common case) or whether this apparently-small difference has deep consequences. Those consequences may not be the fault of either choice (I would bet that the thing we don't understand enough is dependent types, not classical logic), but in a world of partial understanding prudence is still useful.

Yes

Your encoding works fine. You can then write:

run: [Return X]0 -> X
run <return x -> k> = x

I don't think this is really the same as equating X and not-not-X.

But note that this encoding is back in Frank where you already have a distinguished value port. I think an argument can be made that things are nicer and more symmetric if we hadn't done that and just worked with processes. For example, look at the state example from the paper that I copied into my first post here. It handles the yield port and does nothing but pass it along. It didn't need to handle that port at all!

Session Types and Processes

It seems like most of the papers I find have in mind concurrency when they speak of Processes and session types are often pi calculus. I wonder if there's anyone using the using the term the way I've been using the term? Namely:

Process = Message -> (Process, Message)

Lately I've been splitting this into two types, S (sender) and R (receiver) and have been writing A↑B for (A, B) and A↓B for B -> A. So we have:

S = R ↑ M -- A sender is a receiver that has emitted a message
R = S ↓ M -- A receiver is a sender that is waiting for a message

Then receivers are what I originally called process but I also have the name 'sender' for the result of sending a message to a process.

That's the basic idea semantically, but then the trick is labeling messages with ports and only allowing the construction of processes with certain rules that prevent snooping on hidden ports (even counting messages passing back and forth, which can be done generically on any protocol, should be prevented).

Does that sounds familiar at all? Is anyone else looking at effects this way?

Effectful interfaces

The syntax of Frank proposed in the paper actually restricts effectful operations (such as open, write in your example above) to a "pure" interface (A1 -> ... -> An -> B) instead of an arbitrary computation type (A1 -> ... -> An -> [Sigma]B). So your proposed (String -> [Logging]Handle) is not supported for now: catching an operation always gives a value, and handling it cannot add new effects to the ambient ability. (I asked the authors, and) Extending this is future work.

Do you know if the theoretical foundation for this extension is already laid?

With the Process encoding of algebraic effects, there is a subtlety. Consider this fragment:

interface B 
   b : Int -> Int

interface A
   a : [B] Int

handleB: [B] Int -> [A] Int
handleB x = x
handleB <b n -> k> = handleB (k (a + n))

handleA: [A] Int -> Int
handleA x = x
handleA <a -> k> = handleA (k (b 1 + b 2)) -- b is in scope when handling a

foo: [A] Int
foo = handleB a 

bar: Int
bar = handleA foo

EDIT: Forgot to add recursive call to handler

In this example, the computation foo produces an A while it's handling the B response from A. So what should happen? Is this simple non-termination? A run-time error? Something else?

Using Processes as a model for this situation, the correct behavior is error upon attempting to re-enter the A handler while it's in a bad state (still fielding the original query).

Does the category theory that motivated algebraic effects suggest an answer here?

Loop

I vote for non-termination. Here is the reduction sequence I have:

handleA foo
= handleA (handleB a)
= handleA <a -> μx . handleB x>
= handleA (handleB (b 1 + b 2))
= handleA (handleB <b 1 -> μx. x + b 2>)
= handleA (handleB ((a + 1) + b 2))
= handleA (handleB ((a + 1) + b 2))
= handleA <a -> μx. (handleB ((x + 1) + b 2))>
= handleA (handleB (((b 1 + b 2) + 1) + b 2))
= handleA (handleB <b 1 -> μx. (((x + b 2) + 1) + b 2)>)
= handleA (handleB ((((a + 1) + b 2) + 1) + b 2))
= ...

Nitpicking P.S.: in the handleA <a -> k> comment you wrote "b is in scope while handling a". I think this is not completely true: b is "in scope" (in the ambient capability) under the calls to the continuation k, that consumes a <B>Int and returns a [A]Int.

Thanks :)

This reduction sequence and that nitpick were what I needed to read!

This is different than what I've been doing, but I think it's probably better and I can do it with processes, too. I have been working with processes that send and receive messages, but the discpline here is asymmetric. Processes send messages and receive back computations to run. I'd thought of this possibility, but it didn't click.

So to encode this in processes, we just introduce a special process # that runs the messages it receives, producing any side-effects. Then m! is shorthand for # ↑ m [r: \x k. k' x] where k' is the continuation expression in which m! appears. So, in words, we send up m and then wait to receive a computation back which we will run. And we'll run it with a handler that responds to a return message by continuing with the expression k' (discarding k – the computation that issued the return). All other messages before return will be handled by the environment.

Note this convention is more verbose than Frank which just puts ! on nullary operations, but since I use messages as values in the reduction sequence below, I think it's useful to be more verbose. I assume ! binds as tightly as juxt so that you can always stick ! on to the end of an application chain without adding parens.

handleB (b n) k = (k ↓ {ret (a! + n) !}) [b: handleB]

handleA a k =  k ↓ {ret (b 1 ! + b 2 !) !} [a: handleA]

bar
= a! [b: handleB] [a: handleA]
= # ↑ a [b: handleB] [a: handleA] -- I cheated here.  a! should technically catch r and resend it
= # [b: handleB] ↑ a [a: handleA]
= handleA a (# [b: handleB])
= # [b: handleB] ↓ {ret (b 1 ! + b 2 !) !} [a: handleA]
= # ↓ { ret (b 1 ! + b 2 !) ! } [b: handleB] [a: handleA]
= ret (b 1 ! + b 2 !) ! [b: handleB] [a: handleA]
= # ↑ b 1 [r: \x k. ret (x + b 2 !) !] [b: handleB] [a: handleA]
= # [r: \x k. ret (x + b 2 !) !] ↑ b 1 [b: handleB] [a: handleA]
= (handleB (b 1) (# [r: \x k. ret (x + b 2 !) !])) [a: handleA]
= # [r: \x k. ret (x + b 2 !) !] ↓ {ret (a! + n) !} [b: handleB] [a: handleA]
= # ↓ {ret (a! + n) !} [r: \x k. ret (x + b 2 !) !] [b: handleB] [a: handleA]
= ret (a! + n) ! [r: \x k. ret (x + b 2 !) !] [b: handleB] [a: handleA]
= ...

Using a return port (r above) instead of treating the value port specially seems like it might be cleaner. Though I think we really want a different return port for every expression. Also I've been sloppy about ports, just assuming that messages are on a particular port, because I treat port names differently than Frank. Hopefully you get the idea.

There are still a couple of things nagging at me that I seem to lose from my old approach. Maybe I can figure out how to salvage the good stuff.

Minor feature

It occurs to me that the algebraic effect approach of singling out the return port misses out on one simple feature we get for free if we don't distinguish the return port: mid-procedure return. If return is an ordinary port, we can raise return early and it works just as imperative programmers would expect.

Session Types and Processes

You might like then

Parameterized extensible effects and session types (presented at TyDe 2016). It even features the internal choice.

The idea of effects and processes is very old -- going back to Petri and Actors. The web page
Having an Effect is dedicated to that idea, clarifying some historical connections. I gave this talk three times already.

More details

Thanks Oleg for the links. I can believe that the idea of effectful computations as processes is quite old. This was one of my first ideas for what I wanted in my own programming language, ~20 years ago. (It looked much different back then).

But I wonder whether anyone has studied a setup with ports the way I'm discussing. It seems very close (perhaps identical) to algebraic effects. I can sketch it pretty simply here. I'll use variable r for a receiver, which is a function from a message to a sender, which is a (message, receiver) pair.

Two simple operations that we expose are r ↓ m and r ↑ m. The former sends a message into a receiver and the latter pairs an upward message to a receiver that will receive the response. Both of these constructions produce senders. Rather than naming senders, I will generally pattern match on r ↑ m (a pair).

Then we have handlers that wrap processes. We allow upward handles, written p [a↑: f], that catch messages arising from the nested process p, and downward handlers, written p [a↓: f] that catch messages coming downward from above. And here p can be either a sender or receiver. So we have four cases (sender/receiver and up/down), but the rules for the semantics of handlers are simple:

(r ↑ m) [a↑: f] = f r m   if m is on port a
                = r[a↑: f] ↑ m  otherwise -- message passes up

r [a↑: f] ↓ m = (r ↓ m) [a↑: f] -- downward messages pass by up-handler
                
(r ↑ m) [a↓: f] = r [a↓: f] ↑ m -- upward messages pass by down-handler

r [a↓: f] ↓ m = f r m   if m is on port a
              = (r ↓ m) [a↓: f]  otherwise -- message passes down

When an upward handler gets a message from below, it handles it if it's on the correct port, otherwise passes it up. When an upward message handler receives a downward message, it always passes it downward without handling it. And so on.

Just to emphasize, the rules above define the semantics of handlers, but then we have to use only these handlers (and r ↓ m and r ↑ m) to build up processes. We're not allowed to pattern match an arbitrary sender with r ↑ m as above, because that would require knowing about messages on hidden ports. Care was taken so that handlers only get to see messages that arrive at their port, and then the result of the handler function should be a process that preserves expected protocol on the hidden ports.

To that end, we can type handlers with a schema like this (other cases are similar):

r : R e    f : R e -> m -> S (e' + a::P.m)    e' > e
----------------------------------------------------
              r [a↓: f] : R (e' + a::P)

Some notes on what this means:
- R ps and S ps represent receivers and senders on a set ps of ports with protocols
- Addition is type level set append.
- a::P means port a follows protocol P
- P.m is the protocol remaining to be followed by P after a transition of message type m (or a type error if that message type isn't allowed as the head of the protocol).
- e' > e means e' has at least the ports of e with the same protocols.

Is this clear? Is this interesting to anyone? I have a paper in the works on how to use this construction in an effect system, but is this core construction described somewhere?

Not sure

I personally think that you should look in more details at the work on session types. Unfortunately, I'm not super familiar with them myself so I cannot precisely comment on where to look. But I know that a list of messages (or effectful operations) one expect to receive, or send, with a static description of the interaction protocol, all that has been described in the session type literature. Another aspect of session types is that you can often compute, from a static protocol description, the "dual" protocol corresponding to the other corresponding entity, by inverting inputs and outputs -- I suppose you could do this here as well.

One the other hand, the use of session types that I know of do not have the "pass more in depth" behavior on messages that they don't understand; in typical process calculi, people waiting on a given message will typically block, but you have a set of such processes that are parallel to each other and you expect that one of them will consume the message. The behavior of accepting several messages simultaneously, as with effect handlers, is in fact more actor-like, although there more structure on the receiver hand (not just a list of accepted messages, but an ordering between the various handlers that can restart computation at different points).

Pi calculus

Everywhere I look, session type means pi calculus. Is that always true? I've commented a bit here about the relationship I see between my processes and pi calculus. I think the main difference is that I focus on the state of the port, whereas pi calculus focuses on the state of the process. I'm not an expert (by any means) on pi calculus, but it seems very powerful (e.g. able to encode concurrency) and very complicated for use as an effect system. Compare to what a protocol for me might look like with my style processes:

protocol State a
    get: Yield a (State a)
    set: b -> Yield () (State b)

protocol Yield a P
    yield: a -> P 

Protocol declarations would serve a purpose very similar to interface declarations in Frank. They explain the messages that can travel over a port in a given protocol and tell which protocol comes next. The above is a type state protocol for interaction with a mutable cell. (I'm assuming a notation here that implicitly inserts alternation -- otherwise you might expect to see a minus sign before those uses of Yield to indicate that the messages of yield go the other way. I think this might be useful sugar since alternation is the common case).

So I don't really see session types as a viable alternative for direct use in a practical effect system. The notion of process I have in mind seems more akin to algebraic effects. And from my present understanding, it seems to both generalize and simplify the algebraic effects approach. That makes me think people just aren't aware of this construction. I'll try to clean up my paper and put it on Arxiv this week. (Anyone can feel free to harass me if I don't.)

Resources

In the future work section, the Frank paper mentions borrowing the concept of resources from Eff. The citation writes this:

When the toplevel evaluation encounters an operation n # opi e′, it evaluates ci with x bound to e′ and y bound to the current resource state.

Between that and the example of how to model ML references, it seems to me that this is proposing global state. Does someone know if that's right? For example, is it possible to capture a computation that uses resources as a value in a way that captures the resource state as part of the value?

How global?

It depends on how "global" you have in mind. Resources, if I understand correctly, allow you to store some state on the stack at the place where the handler is installed (in this regard they are similar to Racket's "stack marks"). But once this stack frame is popped, the resource is gone -- unlike a heap in a ML language that lives independently of control. Besides, someome between you and the handler may install a more local handler to catch these operations.

On the other hand, resources in Eff are somewhat bundled with "instances", which let you dynamically create a new set of operations (a new instance of a given effect signature) whose identity is generative: it is incompatible with all previous instances of the same operation. This lets you create private operations that nobody else can raise/handle (unless you let them); so, in particular, if you set a handler for them at the top of the stack, you can pass down values that raise them and that you know will never be intercepted by some other handler, letting you have a sort-of-global effect.

Are you sure?

If you look at section 6.3 (state example), there is this text:

An even bigger problem is that the reference may propagate outside the scope of its
handler where its behaviour is undefined, for instance encapsulated in a λ-abstraction.
The perfect solution to both problems is to use resources as follows:

let ref x =
  new ref @ x with
    operation lookup () @ s -> (s, s)
    operation update s’ @ _ -> ((), s’)
  end

I interpreted this to be saying that they want the reference to outlive the handler that you might install there where you create the reference. And the fact that the 'with' clause is attached to the syntax of 'new' suggests to me that there maybe isn't any way to handle these references. It's a way to generate a reference that uses global state and doesn't need to be handled.

Based on that reading, it seems easy enough to extend this approach to not use global state. Rather than allocating references from a global heap, you could make heap access (new) itself an effect. Then you can allocate from a heap (or several heaps) and put each heap somewhere on the handler stack - nothing global.

But I want to make sure I'm not missing the point. Maybe the resources already are somewhere on the stack and I've missed their & your point. (BTW if you know of any other references that explain resources, that would be great).

Hm

Indeed it seems that I misunderstood: your snippet seems to suggest that handlers are attached to the operations in this case, and will be used when the operation reaches "the top" of the stack, making it more convenient to use them as global state. (But again it seems to be more a property of "dynamic effect" / instances than of the idea of resources themselves, which just tracks state across the activations of a given handler.)

Cofunctions and type classes

It seems to me the behaviour can be split into type-class dispatch, and a cofunction to maintain the state. The cofunction is a simple loop (tail-call) that receives the commands and returns the results. With this model the commands themselves would be simple datatypes.

Edit: I will add an example of a cofunction,where 'yield' returns its argument to the caller of the current function (like "return"), and accepts the next call to the cofunction (JavaScript like language).

data Op<A> = Lookup | Update(A)

ref(x : A) =>
   refLoop(x, yield(null))
   where
      refLoop(x, op : Op<A>) =>
         match (op)
            Lookup => refLoop(x, yield(x))
            Update(y) => refLoop(y, yield(null))

test() =>
    ref(0)
    ref(Update(27))
    ref(Update(13))
    ref(Lookup)

Test would return "13". The cofunction allows state to be expressed as a tail call, which can be optimised away. Effectively the the closure behaves like an abstract datatype. The interesting thing is an ADT is a simple recursive cofunction, but more complex protocols are possible.

A further thought is that it is not far from this to stateful objects, where the methods are the commands, and the object state is passed recursively. The question is then are simple objects (no inheritance) easier to use? They are certainly easier to type because the accepted set of commands cannot change depending on the internal state of the cofunction. You would end up with something like a 'neater' version of JavaScript :-)

Manually threading state

This approach requires you to manually thread the reference state through the program, though, so it's not really behaving as a reference but more like a single object container. I think if you try using this as a reference in a larger example then you'll see the problem. Also, if you haven't looked into algebraic effects yet, I would recommend it! I think this Frank paper is a good place to start.

Type Classes

Notice algebraic effects = type classes + cofunctions. The cofunction above is more like an abstract datatype than an object, as it only has one instance. "ref" has one state shared by all uses of the cofunction, so you do not need to create a new instance of it. Take the example above and add a typeclass to make dispatch implicit and you get:

typeclass Ref
   lookup() => ref(Lookup)
   update(x) => ref(Update(x))

test() =>
   update(13)
   update(27)
   lookup()

It only has one instance, so default implementations are used.

Edit: I am not sure you have understood the original example, "ref" does not have to be threaded as it's a top level function/cofunction. You can do:

test1() =>
   ref(0)
   ref(Update(27))
   test2() // note no threading

test2() =>
   ref(Lookup)

Oops

Sorry, I thought the consecutive lines of ref were function application doing the threading. I see what you mean. I agree that this scheme seems roughly equivalent.

One initial reaction I have is that it seems to require co-functions, which involve spooky action at a distance, to be woven into the fabric of values. One nice thing about algebraic effects (or my processes) is that they make sense as "values" that emit messages to be handled. If you have an effectful computation, that should be reflected in its type. If you can cook up a scheme to keep track of which co-functions a given computation interacts with, I suspect it will look very much like algebraic effects.

It just occurs to me that this concern about typing might equally apply to resources. I wonder if Eff tags computations with "uses global state" if they've used resources.

Typing Cofunctions

Type-classes would track the co-functions, so a function that uses them would have those type-classes as constraints. By default functions are polymorphic in type-class bounds (if we have type-class inference), so functions behave like Frank "A -> []B" types. If you supply type-class bounds, then obviously they don't get inferred, so "(Ref A) => A -> A" would behave like Frank "A -> [Ref]A".

Typing cofunctions is not straightforward, and seems to require dependent types. When you first call "ref" it has the type (using Int for simplicity although it is polymorphic in the above definitions): "Int -> ()", however next time you call it you need to pass an "Op", and what you get back depends on the value of Op. Notice also you can think of calling the cofunction as passing a message of type "Op" to the resource (IE a cofunction behaves like a resource) so "Op.Lookup -> Int" and "Op.Update -> ()", the loop above then stays in the state expecting another "Op".

If we promote the "Op" messages to types then we can avoid dependent types, but we then need to introduce type-cases to the language.

data Lookup = Lookup
data Update<A> = Update(A)

ref(x : A) =>
   refLoop(x, yield(null))
      where
         refLoop(x, op : Op<Lookup \/ Update<A>>) =>
            typematch (op)
               Lookup => refLoop(x, yield(x))
               Update(y) => refLoop(y, yield(null))

Now I am not really sure how to write the type, but the first call to "ref" has type "Int -> ()" and then every subsequent one has the type "Lookup -> Int /\ Update Int -> ()". Perhaps we could represent this sequence of types as a list:

ref : [Int -> (), Lookup -> Int /\ Update Int -> (), ...]

It becomes like typing a protocol at this point. Has any work been done on typing protocols?

Typing protocols

Well sure, Hoare did in CSP. You're basically saying the type of a process is the set of all possible event sequences the process can engage in.

I am currently looking at CFG's (and indeed regexps) as reasonably simple ways to express such sets in the simpler CSC (communicating sequential coroutines) system. For example a coroutine implementing a partial function of a stream goes read, maybe write, go back for more, and the type is given by regexp (R+W)+ where postfix + means repetition. Obviously the notation gets messier for multi-channel coroutines and its not clear to me what "type checking" a composition such as a pipeline of transducers actually means.

Where do co-functions live?

As I think about this a bit more, the big problem I'm having is trying to figure out where your co-functions live. "Globally" is not a good answer! Relatedly, with algebraic effects you have a type for a computation with unhandled effects. But once you've handled an effect, you generally want it removed from the type - locally handled effects are nobody's business. So it seems like you don't want to type interaction with a (locally bound) co-function. You just want to type interaction with a named but unbound co-function.

Also, I don't think you need dependent types or type-case. You can use GADTs to keep track of what the message does to the protocol state as part of the message type.

GADTs

You are right about GADTs, I had thought that, then forgot about it :-)

Also functions/cofunctions are first class, so you can pass them as arguments, its just convention that top level things are global.

Lost

I'm lost trying to figure the semantics of your first Ref example. How does the second call to Ref interact with a co-function instead of creating a new reference? Also, would you mind doing an example where a function creates a local reference and uses locally?

Cofunction Semantics

The semantics are like a coroutine, but always with function call semantics. So when you call 'ref' you pass arguments like a normal function, when 'ref' yields it returns the parameter of yield to the caller, but also saves the re-entry point. When 'ref' is called again, it continues from where it left off, returning the arguments passed to 'ref' as the result of 'yield' so from inside 'ref' yield behaves like a function call. Its probably easiest to explain the control flow in the first example (We can interpret the newline the same as Frank with snd(x, y) = y):

data Op<A> = Lookup | Update(A)

ref(x : A) =>
   refLoop(x, yield(null)) // 1
   where
      refLoop(x, op : Op<A>) =>
         match (op)
            Lookup => refLoop(x, yield(x)) // 2
            Update(y) => refLoop(y, yield(null)) // 3

main() =>
    ref(0)
    ref(Update(27))
    ref(Update(13))
    ref(Lookup)

Assuming we start at 'main' the control flow is:

- calling 'ref(0)' passes 0 into 'ref' as x
- 'ref' gets to 'yield(null)' (labelled '1'), returns the null, and internally saves the continuation.
- main calls 'ref(Update(27))' which re-enters 'ref' by returning 'Update(27)' from the yield, and passing this along with the value of 'x' to 'refLoop'
- 'refLoop' matches on 'op' and takes the 'Update' branch.
- gets to 'yield(null)' which returns null from the call to 'ref(Update(27))'
- 'main' calls ref(Update(13)) which returns from the 'yield(null)' (labelled '3') with the value 'Update(13)' which is passed to refLoop in the tail-call along with the value of 'y'
- the match takes the 'Update' branch.
- returns from call 'ref(Update(13))' with null
- main calls 'ref(Lookup)'
- returns from call to 'yield(null)' (labelled '3') with the value 'Lookup'
- calls 'yield(x)' (labelled '2') which returns from 'ref(Lookup)' with the value '13'.

Does that make sense?

Thoughts

I get the idea, but the syntax doesn't make sense to me yet and I think it may have bugs. Does the => syntax install a process in an environment and give it state? It seems to with the ref() declaration, but not with the refLoop() declaration (why doesn't the yield in refLoop yield back to ref?)

Also, the fact that the initialization is treated the same way as message passing seems kind of ugly to me.

I think you could maybe clean up both issues by letting 'run c expr' install and run a co-routine with body exp in an environment under name c?


-- These are just *functions* at this point:
ref x:A = refLoop x (yield null) where
  refLoop x op = ...

main =
    run r (ref 0) -- binds r to the continuation, evals to the first yield (null in this case)
    r (Update 27)
    ...

This has the nice effect that r always has the same continuation type, because we didn't try to type the "initial coroutine" -- we only need to type it at the first encounter of yield. It's now practical to skip complicated protocol typing if you want to, since you can do practical things with a uniform interface type.

It also makes explicit where the co-routine boundary is (it's at run). But you also need to explain what the behavior is when 'r' escapes this lexical environment.

Simpler

'=>' is just regular function/cofunction definition. There is no state apart from the cofunction 'continuations'.

I can use a more Haskell like syntax, so the above would be:

data Op a = Lookup | Update a

ref x = refLoop x (yield ())
   where
      refLoop x Lookup = refLoop x (yield x)
      refLoop x (Update y) = refLoop y (yield null)

test = let _ = (ref 0) in
   let _ = (ref (Update 27)) in
      let _ = (ref(Update 13)) in
         ref(Lookup)

A better way to define it which does what you want without introducing a magic 'run' keyword would be:

ref(x : A) => (op) : Op<A> =>
   match (op)
      Lookup => ref(x)(yield(x))
      Update(y) => ref(y)(yield(null))

Which you would write Haskell style as:

ref x = \op -> case op of
    Lookup -> ref x (yield x)
    Update y -> ref y (yield null)

let r = ref 0 in 
   let _ = r (Update 27) in
      let _ = r (Update 13) in
          let z = r (Lookup)

What does yield do?

What does yield do (precisely)?

Yield

yield returns control to the caller with the value of its arguments as the result, but it also updates the function entry point, so the arguments of the next call to the function are returned from that yield.

In terms of implementation, the function call would have to indirect via a pointer that initially points to the start of the function, but gets updated by yield. You could view this as a small single element stack where on function entry it pops the current address and jumps to it, and on yield it pushes the 'return' address to jump to the next time you call the function.

Yield returns control to the caller

... of what?

helper x = ... yield null ...
ref x = ... helper x ...
foo x = ... ref 0 ...

yield

yield returns control to the caller of the cofunction in the same way that in C a return returns control to the caller of a C function: the return address (continuation) is saved somewhere implicitly (such as on the machine stack).

This limits what cofunctions can do (form trees of control) compared to general coroutines which do read/write on channels, where the channels explicitly hold the peer continuation. However the advantage is simplicity and syntactic unification.

Single Thread of Control

What I like about it is that there is a single thread of control and you cannot get deadlocks, which I don't think is the case with general coroutines.

The Cofunction

Where "return" would return to :-) Consider JavaScripts "return" statement, it is imperative because it is not a function. In my example "yield" looks like a function to the callee, but it serves the purpose of "return". So "yield null" returns "null" from the call to "helper x".

I guess your point is what happens with nested functions and cofunctions? In the syntax above a thing that "yields" is a cofunction, so that issue does not arise.

Edit: An orthogonal point which might be confusing is how you distinguish the value of a function from a reference to the function. Frank does this by treating an unapplied function as a reference to the function, and only as its result value when all the arguments have been supplied. This leaves an anomaly with zero argument functions, hence the need for the "!" postfix to indicate execution of a zero argument function (without the "!" it is a reference to the function). If we use '()' for argument lists in the style of 'C' then we do not need anything else because:

f() => 27 -- define a function that returns 27

f   // reference to the function
f() // execute the function (like Frank's "f!")

This distinction applies equally to multi-argument functions.

Also where Frank uses "let g = {f x}" to defer execution, you can use a lambda in the same way. For example this could be written"

let g = () => f(x) // equivalent to Frank's "let g = {f x}"

This is semantically the same, as in Frank 'g' would be executed with "g!" and in this syntax "g()"

Edit2: You can also program with only cofunctions, as a normal function is a special case of a cofunction that looks like this:

id x = id (yield x)

Hmm

Is this standard terminology? Google didn't turn up much interesting for "co-routine vs. co-function". I'm familiar with Python generators... I'd suggest you not copy them (for example, in python nested functions can't close over yield). I'm also not sure why you think co-routines would be multi-threaded or suffer deadlocks.

If your language already supports mutable bindings, I can understand why you want to keep the continuation state in the environment. I still think you're not thinking clearly about where yield is supposed to go. You gave this example:

ref(x : A) => (op) : Op<A> =>
   match (op)
      Lookup => ref(x)(yield(x))
      Update(y) => ref(y)(yield(null))

Apparently this yield is supposed to resume control to the caller of the nested function. Earlier control was apparently passing to the caller of the top-level function. It seems to have "do what I mean" semantics.

It seems to me that you're going to want all of these cases:
- nested helper functions that yield back to their parents (like refLoop)
- functions that help construct co-functions (like the example here)
- functions that construct and use co-functions locally

To accommodate these cases, I think you need some kind of syntax that indicates where a new yield-scope is introduced. Thus the 'run' I proposed. I made it an expression to remove the asymmetry between the initial continuation (an explicit function) and subsequent (implicit continuations of yield), but if that doesn't bother you there are lots of choices. I think you need something, though.

Some final notes: in order to have the same expressive power as algebraic effects, you'll need to support capturing a co-function in its mutated state as a value (you already have a syntax for that -- naming it without parens).

You also need to figure out if you're going to support passing access to co-routines of the environment into a co-routine and what the syntax for that would look that. In effect language this corresponds to my initial discussion with gasche in this thread about passing effects from a handler back to the initial effect-raising environment.

I would embed functions into co-functions by:

nocontinue: (forall a. a) -> ()
return x = nocontinue(yield x)

Good luck!

cofunctions vs coroutines

Cofunctions is not standard terminology, but it came up in discussion with John Skaller.

Regarding deadlocks, generalised coroutines can suffer deadlocks as a function can be waiting on a queue that is waiting on that function to output something. John's generalised coroutines can deadlock I think, so don't get too distracted by my reply to him which does not apply to simple co-routines like Python's yield.

Apparently this yield is supposed to resume control to the caller of the nested function. Earlier control was apparently passing to the caller of the top-level function. It seems to have "do what I mean" semantics.

That's a good catch, I think the earlier version would not have worked. It was a bad translation from an imperative loop.

To accommodate these cases, I think you need some kind of syntax that indicates where a new yield-scope is introduced. Thus the 'run' I proposed. I made it an expression to remove the asymmetry between the initial continuation (an explicit function) and subsequent (implicit continuations of yield), but if that doesn't bother you there are lots of choices. I think you need something, though.

I don't mind it - I think an alternative is to mark the co-function definition somehow. The problem with allowing nested functions is you will need a stack for the cofunction.

I think it may be simpler to say I wrote the first example too quickly and it should not work. Of your three cases I think you need (2) and (3), but I think you can do without (1), as we want the cofunction state to be fixed size. Maybe there is a better solution with more thought.

In effect language this corresponds to my initial discussion with gasche in this thread about passing effects from a handler back to the initial effect-raising environment.

That's why I mentioned it, there seemed to be similarities to your discussion.

You also need to figure out if you're going to support passing access to co-routines of the environment into a co-routine and what the syntax for that would look that. In effect language this corresponds to my initial discussion with gasche in this thread about passing effects from a handler back to the initial effect-raising environment.

I thought I would just pass a reference to a cofunction like passing a function.

test1() =>
   let x = ref 0
   x(Update 13)
   test2(x)

test2(y) =>
   y(Update 25)
   y(Lookup)

Fixed state cofunctions

...will be fairly limiting compared to algebraic effects. It means you can't take a computation that generates some effects and handle some of them by yielding. e.g. suppose you have a computation that generates "print" effects, and you want to convert that into a generator that enumerates the printed things.

The issues with passing co-function references are 1) syntax and distinguishing it from passing the captured co-function value and 2) typing and/or dealing with escaping references.

Static Scoping and Shadowing.

I would imagine that print is a cofunction that encapsulates the state of the IO stream. Assuming I want to avoid dynamic scoping, and we allow shadowing of variables we can do:

print(s) => ... // do IO
   myScope() =>
      print(s) => .. // log
      
      print("hello")
      print("world")

The idea is there is no global state, any state has to be encapsulated in a cofunction. This means the state of the IO streams is wrapped-up inside of 'print'.

Also

Responding to your edit, I'm still not sure that you're being careful about where the state lives. From everything you've said thus far, I'd expect this behavior:

test1() =>
   let x = ref 0
   let y = ref 0
   x(Update 13)
   let z = y(Lookup) -- z = 13 (!)

One State

Yes, I think so too, that is why I said it was more like an abstract data type rather than an object.

Edit: I think simple objects probably present a more understandable model of state. We could get something easily modeled by cofunctions that looks like a simple object. You would have methods that have immutable local variables, and all mutable state would have to be object properties.