Interpret a `Sem (x ': r) a` into a `Sem (y ': r) b`?

109 views Asked by At

I'm trying to put together the machinery to write something like secret-sharing (e.g.) using algebraic effects. More specifically I'd like to be able to write the protocol in terms of the actions of each individual party, and then handle that effect-space into a simulation of some number of actors all talking to each other.

I want to use algebraic effects because I think it's cool, and I think it will help with some of the subsequent analysis. Polysemy seems like a good choice of library.

As an example, consider the simple case of three parties trying to get the sum of their secret inputs. We might write something like

import Polysemy (Member, Members, Sem, makeSem)
import Polysemy.Random (Random, randomR)

data Communication3 s m a where
  Message :: (s, s) -> Communication3 s m (s, s)  -- Pass a message, and get peers' messages.
  Secret :: Communication3 s m s                  -- Input one's own secret values.
  Reveal :: s -> Communication3 s m (s, s)        -- Share a value with all peers, and get theirs.

makeSem ''Communication3  -- Uses template haskell to generate:
-- message :: Member (Communication3 s) r => (s, s) -> Sem r (s, s)
-- secret  :: Member (Communication3 s) r =>           Sem r s
-- reveal  :: Member (Communication3 s) r => s ->      Sem r (s, s)


--------- The "application" code: --------

modulus = 1013 :: Int
modulo = (`mod` modulus)
randomM :: Member Random r => Sem r Int
randomM = randomR (0, modulus - 1)

sumOfSecrets :: Members [(Communication3 Int), Random] r =>
                Sem r Int
sumOfSecrets = do
  myInput <- secret
  noiseB <- randomM
  noiseC <- randomM
  (shareInB, shareInC) <- message (noiseB, noiseC)
  let shareInA = modulo (myInput - noiseB - noiseC)
  let shareResultA = modulo (shareInA + shareInB + shareInC)
  (shareResultB, shareResultC) <- reveal shareResultA
  return $ modulo (shareResultA + shareResultB + shareResultC)

(Whether or not the above is any good would be good to know, but not the question here. It does typecheck, once you get Stack to compile polysemy-zoo.)

How would I write a handler for the Communication3 effect?

If we imagined we were trying to implement this as an internet protocol, then the "executable" would look a lot like the code we've written; messages would get handled into whatever process for sending and receiving data over the wire.
But I also (in fact, primarily) want to be able to simulate the three parties locally. That means, roughly speaking that I need to write a handler/interpreter/runner like

runCommunication3 :: Sem ((Communication3 a) ': r) b -> Sem r (b, b, b)

representing running the whole thing three times (mostly) in parallel.

Clearly this is possible to do; the State handlers do it. But I haven't been able to find any documentation of how. Where should I be looking? What am I missing?

0

There are 0 answers