Communicating systems require channels to communicate, in many of the programming languages that provide communication channels the management of these channels at the application layer is left to the programmer to get right. That is, the programmer is responsible for ensuring that the channel is established, connected to, and then destroyed.
In languages that support dependent types we can encoded, at the type level, extra properties about our software program. Further, the idea of algebraic effects supports the separation of a program's description from its realisation in different contexts. Edwin Brady's
EFFECTS library has shown how this is possible using dependent types . The implementation of
EFFECTS allows for efficient management of a program's side-effects and dealings with the outside world. See the Effects Tutorial for more information.
An interesting aspect of
EFFECTS is that each effect is associated with a resource. For the
FILE effect it is a file handler, for the
PERF effects that I contributed to
EFFECTS it is logging levels and captured metrics. With resource based algebraic effects we can capture (at the type level) the allowed (state) changes to this resource. If we examine the current
FILE effect from Idris' effects library you can see this for file access. The resource for the
FILE effect is the file descriptor and its relation to the mode of operation.
||| The file handle associated with the effect. ||| ||| @m The `Mode` that the handle was generated under. data FileHandle : (m : Mode) -> Type where FH : File -> FileHandle m
FILE effect is a dependent effect in that the result of the effectful operation is used to calculate the value of the resource being computed over. Given the function
calcResourceTy : (m : Mode) -> (ty : FileOpReturnTy fOpTy retTy) -> Type calcResourceTy _ (FError e) = () calcResourceTy m _ = FileHandle m
calcResourceTy computes the type of the resource as being unit if there is a failure, and if not the resource is the
FileHandle parameterised by the mode of operation. When combined with the mode of operation we can have a more informed means to calculate the next value of the resource.
||| An effect to describe operations on a file. data FileE : Effect where -- Open/Close Open : (fname : String) -> (m : Mode) -> sig FileE (FileOpReturnTy SUCCESS ()) () (\res => calcResourceTy m res) ....
But why talk about the
FILE effect? Well if we think about it, reading and writing with a file is analogous to communicating over a channel. We have to:
So why not apply creation of a file effect to management of a communication channel?
Fortunatly, Idris comes with an unsafe means to perform concurrent communication between different Idris processes (and IPC too). Edwin has shown how we can reason about communication in Idris at Lambda World, and spoiler alert in the TDD book too.
However, over the summer I took a stab at using effects to manage channels. This was inspired by earlier work by Simon Fowler.
For the remainder of this post, I shall describe my implementation of a resource based algebraic effect for channels.
FILE effect we are going to model an active session using a simple resource
OpenSesh, and parameterise it by the state of the channel represented by the enumerated type
data SSTATE = Unconnected | Spawned | Active
Channels are either: Unconnected---literally unconnected; Spawned---alive but not communicating; or Active---are communicating with another entity.
OpenSesh is defined as follows:
data OpenSesh : (st : SSTATE) -> Type where NoSesh : OpenSesh Unconnected SpawnedSesh : (pid : PID) -> OpenSesh Spawned ActiveSesh : (pid : Maybe PID) -> (sesh : Channel) -> OpenSesh Active
Here an unconnected channel is specified using
NoSesh and contains no information.
SpawnedSesh represents a spawned process, so we must capture the processes
ActiveSesh represents either a client channel or server channel. If the channel is connecting to another process, not only do we need the channel to communication on, but also the
PID of the process. If we are the server process, we need to keep track of the communication channel only.
Before we define the effect we first define some helper code.
First, type synonyms.
INIT : Type INIT = OpenSesh Unconnected WAIT : Type WAIT = OpenSesh Spawned ACTIVE : Type ACTIVE = OpenSesh Active
The allowed state transitions between resource types. We have decided that we shall use a
Bool to describe success or not.
As a Client
If connection was successful then move to active, otherwise go back to wait.
connectedOK : Bool -> Type connectedOK False = OpenSesh Spawned connectedOK True = OpenSesh Active
As a Server
If attempt to listen was successful then move to active, otherwise go back to unconnected.
listenedOK : Bool -> Type listenedOK False = OpenSesh Unconnected listenedOK True = OpenSesh Active
If message was sent then stay active, otherwise there was a failure and move to unconnected.
sentOK : Bool -> Type sentOK True = OpenSesh Active sentOK False = OpenSesh Unconnected
If message was received then stay active, otherwise there was a failure and move to unconnected.
receivedOK : Maybe a -> Type receivedOK (Just v) = OpenSesh Active receivedOK Nothing = OpenSesh Unconnected
With the helper code defined, we can now describe an effectful means to manage processes. To do so we have to use a mutual block to allow an effectful process to spawn a second effectful process.
mutual ProcessE : (st : Type) -> (rTy : Type) -> (inEffs : List EFFECT) -> (outEffs : List EFFECT) -> Type ProcessE st ty inEffs outEffs = Eff ty (CHANNEL st :: inEffs) (\_ => (CHANNEL st :: outEffs)) ||| The effectful description for `Session`. data ChannelE : Effect where ||| Spawn an effectful process to communicate with, transitioning ||| from `INIT` to `WAIT`. Spawn : Env IO esi -> ProcessE INIT () esi eso -> sig ChannelE (PID) (INIT) (WAIT) ||| Connect to a spawned process, transitioning from `INIT` to ||| result of `connectedOK`. Connect : sig ChannelE (Bool) (WAIT) (\res => connectedOK res) ||| Listen for a connection, traisitioning from `INIT` to result ||| of `listenedOK`. Listen : (tout : Int) -> sig ChannelE (Bool) (INIT) (\res => listenedOK res) ||| Send a message of type `a`, transitioning from `ACTIVE` to ||| result of `sentOK`. Send : a -> sig ChannelE (Bool) (ACTIVE) (\res => sentOK res) ||| Receive a message of type `a`, trasitioning from `ACTIVE` to ||| result of `receivedOK`. Recv : (a : Type) -> sig ChannelE (Maybe a) (ACTIVE) (\res => receivedOK res) ||| End a session, trasitioning back to `INIT`. End : sig ChannelE () (ty) (INIT) ||| An effectful API for `System.Concurrency.Sessions`. ||| ||| @st The state the session is in. CHANNEL : (st : Type) -> EFFECT CHANNEL st = MkEff st ChannelE
If we examine the description of the effectful functions, we can see the allowed state transitions between different API calls. For example, spawning a process will transition the effect from being unconnected to waiting. Then we can only progress to an active session if connecting to the spawned resource was successful. Similar transitions are encoded in the effect between the different operations.
With the effect specified, we can now define an implementation for this effect for the
IO context. This handler will describe how to realise the management tasks described in the effect. For concurrent processes this will require spawning processes, connecting to processes, listening for processes, sending and receding messages, and closing sessions down.
Handler ChannelE IO where handle NoSesh (Spawn env proc) k = do pid <- spawn $ runInit (NoSesh::env) (proc) k (pid) (SpawnedSesh pid) handle (SpawnedSesh pid) Connect k = do msesh <- connect pid case msesh of Nothing => k False (SpawnedSesh pid) r@(Just res) => k True (ActiveSesh (Just pid) res) handle (NoSesh) (Listen tout) k = do msesh <- listen tout case msesh of Nothing => k False NoSesh r@(Just res) => k True (ActiveSesh Nothing res) handle st@(ActiveSesh pid sesh) (Send m) k = do sent <- unsafeSend sesh m if sent then k True st else k False NoSesh handle st@(ActiveSesh pid sesh) (Recv ty) k = do res <- unsafeRecv ty sesh case res of Nothing => k Nothing NoSesh (Just val) => k (Just val) st handle st End k = k () NoSesh
With the effect and handler defined, we can now present the API that the developer can use to program with.
Process is a function that can communicate using the session effect. We use this alias to make describing communicating processes that little bit easier.
Note that the definition of
Process already specifies the session required for communicating.
Process : (st : Type) -> (rTy : Type) -> (es : List EFFECT) -> Type Process st ty inEffs = ProcessE st ty inEffs inEffs
Attempt to spawn an effectful process that communicates using a
Sessions. Returning the
PID of the spawned process.
spawn : (env : Env IO es) -> (proc : Process INIT () es) -> Eff (PID) [CHANNEL INIT] [CHANNEL WAIT] spawn env proc = call $ Spawn env proc
Attempt to establish a connection to the spawned process. The function can only be used once a session has been spawned.
connect : Eff (Bool) [CHANNEL WAIT] (\res => [CHANNEL (connectedOK res)]) connect = call $ Connect
Listen for a fixed amount of time for a connection from an external process. The function is used by the spawned process to accept incomming requests.
listen : (timeout : Int) -> Eff (Bool) [CHANNEL INIT] (\res => [CHANNEL (listenedOK res)]) listen t = call $ Listen t
Send a message of type
ty. Returning a
Bool describing success.
send : (msg : ty) -> Eff Bool [CHANNEL ACTIVE] (\res => [CHANNEL (sentOK res)]) send msg = call $ Send msg
Expect to receive a message of the specifyed type. This is unsafe as receive expects the incomming message to be of the specified type.
recv : (ty : Type) -> Eff (Maybe ty) [CHANNEL ACTIVE] (\res => [CHANNEL (receivedOK res)]) recv ty = call $ Recv ty
stop : Eff () [CHANNEL ty] [CHANNEL INIT] stop = call End
We finish of this post by showing the code for a game of ping pong.
First we describe the called process
ping : Process INIT () [STDIO] ping = do True <- listen 10 | False => stop True <- send "ping" | False => stop msg <- recv String case msg of Nothing => pure () (Just v) => do putStrLn "Ping received" printLn v stop
Notice, that in the code we have to explicitly stop and terminate the process upon failure. If we remove these statements, the program will not compile as we have violated the transitions described in the effect. Further, if we try to send a message before we have connected, Idris will complain further.
pong is the client process that initiates the game of ping pong.
pong : Process INIT () [STDIO] pong = do pid <- spawn [()] ping True <- connect | False => stop msg <- recv String case msg of Nothing => stop (Just v) => do putStrLn "pong received" printLn v True <- send "pong" | False => pure () stop
Again we must call
spawn before we call
connect and both before we can send or receive messages.
We can play the game of ping pong by running the effectful program specifying that we expect two sessions to be used.
play : IO () play = runInit [NoSesh,NoSesh] pong
This post describes how effects can be used to manage our communication channels. A full code listing is available online.
However, the communication over these channels is not type safe. Edwin demonstrated one means of ensuring such type safe communication at Lambda World 2016. However, there are some other things we can do that are more advantageous and cooler. /Yes, there is more cooler stuff that what Edwin demonstrated at Lambda World./ My research is currently focused on not only how to manage channels using dependent types but how to type check the communication itself.
Hopefully I will blog more about what I am up to, I do have some things in the pipeline that I won't share just yet as they are not complete.
 E. Brady, “Resource-dependent algebraic effects,” in Trends in functional programming: 15th international symposium, tfp 2014, soesterberg, the netherlands, may 26-28, 2014. revised selected papers, J. Hage and J. McCarthy, Eds. Cham: Springer International Publishing, 2015, pp. 18–33.