Mailbox typing and pattern matching

[jasone]

As an offshoot of #147 we delved into the problem of how to support mailbox pattern matching. There are several interrelated problems to solve, e.g.

• What are the semantics for pattern matching on a mailbox? This is certainly different than normal match.
• Do we need special receive syntax?
• How do we assure that messages sent to an actor are always of a type which the actor can plausibly handle?

Mailbox pattern matching iterates over the mailbox messages and extracts the first message which matches a pattern. Absent special syntax this could look something like:

Mailbox.recv_any function
| Os (Accept a) -> ...; Some result
| _ -> None

With special syntax, this could look something like:

receive
| Os (Accept a) -> ... result
| _ -> ...

However there remains the question of how to support blocking/non-blocking/timed-wait receive. As for the question of whether to provide receive syntax, it may in fact be critical to do so in order to get typing correct (see below).

There are some interesting composability problems with regard to message typing. Our intention has long been to have each actor spawn via a module which defines its supported message types. For example (leaving out as-yet-unspecified details):

open import Basis

let A = {|
    type msg =
    | T.msg
    | Hello
    | Echo string
|}

However, our current plan is to deliver asynchronous I/O completions (Os messages as seen above) via the mailbox. Imagine a third-party library which performs asynchronous I/O. If that library's I/O completions were to have the same types as the application's I/O completions, havoc could ensue due to under-specified pattern matches "handling" the library's I/O completions. Furthermore, there is the problem of how to pattern match on just I/O completions (not inter-actor messages) in a type-safe way. This at first seems like a problem that could be mitigated by segregating Os messages from inter-actor messages, but the same problem applies there! That is to say that a third-party library could utilize inter-actor communication (IAC), and that should really be opaque from the application's perspective.

We tentatively settled on a solution based on link-time module dependencies. The idea is to require an actor handle to be converted to a typed value only capable of sending messages of a statically specified type. This conversion can of course fail at run time, in which case messages of the specified type cannot be sent to the actor. Under the covers this conversion is implemented by introspecting the module dependencies for the actor's module type — A in the snippet above — and only converting to types in the transitive closure of A's module dependencies. This does not assure that messages will actually be handled, but it does assure that it's at least plausible for messages to be handled.

Back to the question of receive syntax, it is probably critical to have special syntax so that the association between lexical context and the type being matched on can be enforced at compile time. During discussions we imagined that each module scope would provide a unique message type space. However, lexically nested modules present a challenge to this approach; probably better is to provide a unique message type space only for the outermost lexical module context.

The question of whether to support some sort of multiplexed dispatch to various modules came up. After a bit of cleanup from brain splatter we tentatively concluded that this is equivalent to trying to solve the multiple event loop unification problem. Hemlock's answer to that problem is, "Don't do that; use multiple actors."

[cevans87]

I was considering how to deal specifically with

recieve
| Os (Accept a) -> ...
| Os (Read r) -> ...
...

patterns.

We noticed that it's hard to determine the type of the mailbox when Os effects come into play, and our spitball solution was to just combine them all into a per-module Os type. That's fine, but in the example above, we could sleep forever if we never submitted an Accept or a Read to the Os.

Do we need a way to notice that we have outstanding Os submissions that could even satisfy the receive statement? If there are no outstanding submissions that could possibly satisfy the recieve statement, should it halt?

[cevans87]

I also thought a bit about how to unify the machinery for the cases where you want to receive just the result for the submission we created and potentially lexically bound the future to.

# val read: uns -> File.t -> future (fulfillment (Os read))
let read_fut = read 1024 file

Perhaps we could get the result in one of two ways.

First, getting the result directly from the future.

let read_ful = Fulfilment.of_future read_fut 

or

receive
| fulfillment (Os read) read_ful where Fulfillment.get_future read_ful = read_fut -> ...
| ...

This idea obviously uses a compile-time function to create a type fulfillment (Os read), which I'm not sure we're committing to.

[jasone]

I don't think we should try to protect the application from blocking on message receipt which cannot possibly happen. The more general case of this problem is an application bug due to blocking forever on a message receipt from another actor which will never actually send the desired message.

Re: the future-related ideas, I'm confused because it looks like receive is matching on type rather than value, but pattern matching is value-oriented. Can you modify the example to match on value?

[cevans87]

Can you modify the example to match on value?

Let's see if I can do that and go a little deeper.

module Os:
    module Read:
        module Error:
            type t
        module Id:
            type t = uns

        module Pending:
            type t

            val id: t -> Id.t

        module Fulfilled:
            type t = result Error.t bytes

            val id: t -> Id.t

        val submit: uns -> File.t >os-> Pending.t
        val complete: Pending.t -> Fulfilled.t
        val complete_hlt: Pending.t >hlt-> bytes

    module Pending:
         type t =
           | Read of Read.Pending.t
           | ...

    module Fulfilled:
         type t =
           | Read of Read.Fulfilled.t
           | ...

Basically blocking synchronous use-case.

match Read.submit 1024 file |> Read.complete
  | Error err -> ...
  | Ok b -> ...do something with bytes

Matching on a specific read

let p = Read.submit 1024 file
receive
  | Os.Fulfilled.Read f where Read.Fulfilled.id f = Read.Pending.id p -> ...
  | ...

[jasone]

Semantically this looks good to me. Once we have a few more I/O types to consider as examples I think we should play around with APIs to see if the multi-level Pending/Fulfilled approach covers everything we want it to. If so I think it's a good approach since there's very little inherent runtime overhead.