Local state/located effects?

[edsko]

After seeing the ICFP presentation on HasChor, I thought it might be nice to discuss it in the upcoming Unfolder episode (coming Wednesday).

Motivation

As an example, I wanted to make a simple fileserver, where the client can send filepaths and the server responds with the contents of those files. The example in the repo use readLine for the client to interact with the user, but I wanted to abstract from this, and have the client be a thread that takes instructions through an MVar; this means the client needs some state. Similar, the server needs some state too: it needs to know which directory to use as the root directory to serve files from.

Not so nice solution

However, I couldn't really see an easy way to pass this state to the choreography. I can't take the two state parameters as arguments to the choreography, because the server should not need the client state and vice versa. I can take two located parameters

choreography ::
     FilePath @ "server"
  -> (MVar Instruction, MVar Lazy.ByteString) @ "client"
  -> Choreo IO ()

and pass Empty for the argument that is unused:

clientProcess =
  runChoreography
    cfg
    (choreography Empty (Wrap (instrVar, resultsVar)))
    "client"

but this doesn't feel terribly clean.

Better abstraction?

I tried coming up with an abstraction that makes this a little cleaner. First, hoist:

hoistChoreo :: forall m n.
     (forall l a. KnownSymbol l => Proxy l -> m a -> n a)
  -> (forall a. Choreo m a -> Choreo n a)
hoistChoreo hoist = go
  where
    go :: Choreo m a -> Choreo n a
    go (Return x) = Return x
    go (Do eff k) =
        case eff of
          Local l f  -> Do (Local l (\un -> hoist l (f un))) (go . k)
          Comm s x r -> Do (Comm s x r) (go . k)
          Cond l x f -> Do (Cond l x (go . f)) (go . k)

(this definition is uncontroversial, I think). Then, since the only way to extend the Choreo monad is by picking a different underlying m, I defined

data LocalReaderSig f m a where
  LocalLift :: m a -> LocalReaderSig f m a
  LocalAsk  :: KnownSymbol l => Proxy l -> LocalReaderSig f m (f l)

type LocalReader f m = Freer (LocalReaderSig f m)

liftLocal :: m a -> LocalReader f m a
liftLocal = toFreer . LocalLift

askLocal ::
     KnownSymbol l
  => Proxy l -> Choreo (LocalReader f m) (f l @ l)
askLocal l = locally l (\_un -> toFreer (LocalAsk l))

this then makes it possible to "provide local state", in a somewhat similar fashion to endpoint projection:

hoistLocal :: forall m f l.
     (KnownSymbol l, Monad m)
  => Proxy l
  -> f l
  -> (forall a. Choreo (LocalReader f m) a -> Choreo m a)
hoistLocal l s = hoistChoreo hoist
  where
    hoist :: KnownSymbol l' => Proxy l' -> LocalReader f m a -> m a
    hoist l' = interpFreer $ \case
        LocalLift act -> act
        LocalAsk  l'' ->
            case sameSymbol l' l'' of
              Nothing   -> error "invalid"
              Just Refl ->
                case sameSymbol l' l of
                  Nothing   -> error "irrelevant"
                  Just Refl -> return s

The choreography is now a little cleaner:

data LocalState :: Symbol -> Type where
  ServerState :: FilePath -> LocalState "server"
  ClientState :: MVar Instruction -> MVar Lazy.ByteString -> LocalState "client"

choreography :: Choreo (LocalReader LocalState IO) ()
choreography = do
    serverState <- askLocal server
    clientState <- askLocal client
    ...

It still doesn't feel terribly satisfactory though. Am I missing a more obvious solution?

Proper solution?

It seems to me that the cleaner solution would if the argument to Choreo is an indexed monad of kind Symbol -> Type -> Type. There is no reason to assume that the client and the server require the exact same of effects, after all -- indeed, it seems quite likely that they will not.

[gshen42]

I don't have a more obvious and cleaner solution to this problem. But I really like your idea at the end: making the local monad (the second argument to Choreo) indexed by a location so each node can have different sets of effects. This should be relatively easy to implement. One thing I'm a little unsure of is how well GHC supports this kind of indexed monad. I hope I can express it as simply as you did in your example without using language extensions and tricks.

Also, the Unfolder channel looks cool. I'll definitely check out the new episode when it's out.

[edsko]

Ok, thanks for thinking along! :)

As for ghc support: typically when people talk about indexed monads they talk about monads where bind can change the index, of course, which doesn't work so well with do. Simply having an additional type parameter should be fine.

Incidentally, it seems that this kind of location-specific state should be relatively common? Perhaps the constructors of (@) should be exported from Choreography?

[gshen42]

Incidentally, it seems that this kind of location-specific state should be relatively common? Perhaps the constructors of (@) should be exported from Choreography?

Yes, we'll make that change.

[lkuper]

@edsko Thanks for featuring HasChor on the show, and thanks for all the thoughtful suggestions! We haven't released a package on Hackage yet, so now is a great time to be suggesting API improvements.

[edsko]

My pleasure :) The only other thing that comes to mind that I think you could consider changing is the serialization format from Show/Read to maybe binary or CBOR or something.