I’ve promised this post to quite a few people now, so here it is!

Right, so, continuing with the theme of networking in Idris. Today we’ll be looking at how to make a simple networked game of Pong, using the Idris effects library, and IdrisNet2. As before, you will need:

You can find the code used for this project here. You might also want to look at the Space Invaders example written by Edwin Brady here.

No more heavy lifting: Effects in Idris

The main point of this mini-project is to show how different effects in Idris may interact to make a larger program. Traditionally, side-effecting programming in purely-functional languages such as Haskell has been done using monads and monad transformers, which generally works well for smaller numbers of effects. A state and IO transformer is absolutely fine for most things, for example. The problem comes, however, when combining more than a few effects. There are generally two things that people do in this case: combine everything into one big supermonad with a bunch of different side effects, or allow little lifting operations (liftCGI :: IO a -> CGI a, for example, which would be pretty nasty if a stray putStrLn managed to find its way in there prior to the headers being printed out).

The Idris Effects library makes it easier to just define lots of little chunks of side-effecting functionality, operating using a handler abstraction. Functions specify which effects may be used in their types, and the library lets us do side-effecting operations based on which operations are available. If we try and use and effect that is not available in a particular function, for example, we’ll be told at compile time.

The other really nice thing about effects is that we can associate resources with each effect. Since the values and types of resources may change after each operation, this makes it great for enforcing resource usage protocols. I wrote a fair bit more about this in my earlier blog post, where I wrote about how it may be used to enforce resource usage protocols associated with TCP.

 

The Ingredients

Pong is a great candidate for this kind of example because it’s a reasonably simple game, yet makes use of several different side effects. In particular, we need:

  • SDL for graphics
  • UDP server for receiving status updates
  • UDP client for sending status updates
  • Channel-based concurrency
  • State Additionally, we can use the PacketLang EDSL to provide a structured way of communicating data.

Since we’re using effects, we don’t have to settle for putting this into a state / IO monad transformer, which allows us to separate the networking from the graphics bits of the program, for example. We also don’t need to put in a bunch of explicit lift calls into our code, as this is done implicitly by the library.

Networking and Process-Based Concurrency

Previously, I wrote about networking using TCP. This time, I’ll use UDP.

Idris implements basic typed and untyped message-passing concurrency as a primitive within the runtime system. When writing Pong, the first task was to port this over into an effect, so that it could be combined with the rest of the program. This was thankfully not very difficult at all, as it just required wrappers around the original functions! You can find the Process effect here: https://github.com/SimonJF/IdrisNet2/blob/master/src/Effect/Process.idr.

Processes in this case are parameterised over a particular message type, mTy. The key bits to notice about the library are the type of spawned threads: RunningProcessM : (mTy : Type) ->                   (m : Type -> Type) ->                   List EFFECT -> List EFFECT -> Type RunningProcessM mty m effs effs’ =     Eff m () ((PROCESS (Running mty)) :: effs)              (_ => (PROCESS (Running mty)) :: effs’)

Although it might look a tad scary to start off with, all this states is that RunningProcessM is a type parameterised over the type of message that will be sent over the channel, an execution context m, a list of input effects, and a list of output effects. For example, if we wanted to spawn a very basic process which communicated using strings and could use standard IO functions running on an underlying IO context, we’d make a function of the following type:

myProcessOne : RunningProcessM String IO [STDIO] [STDIO]

Or, since the input and output effects are the same, we could just write: myProcessOne : RunningProcess String IO [STDIO]

To spawn a new process, we require our effectful program to have a Process effect available, and we can use that to spawn new threads using the spawn operation.

setupProcesses : { [PROCESS (Running String), STDIO] } Eff IO ()
setupProcesses = do
  pid_one <- spawn String myProcessOne [()]
  myProcessTwo pid_one 10
  return ()

The spawn operation takes the type of the parameter, the function to spawn in a new thread, and an initial resource environment as its arguments. It returns a handle to the process, in this case of type ProcPID String. It’s then possible to send and receive messages using the sendMessage and recvMessage functions:

myProcessOne : RunningProcess String IO [STDIO]
myProcessOne = do
  msg <- recvMessage
  putStr $ "Consumer process received message: " ++ msg ++ "\n"
  myProcessOne

myProcessTwo : ProcPID String -> Nat -> { [PROCESS (Running String)] } Eff IO ()
myProcessTwo _ Z = return ()
myProcessTwo pid (S k) = do
  sendMessage pid (show k)
  myProcessTwo pid k

You may be wondering what the type of myProcessTwo is. This is best described in the Effects tutorial, but essentially says that the function is an effectual program with the PROCESS effect available and communicating with child processes using Strings, running in the IO execution context.

This should explain the basics of channel-based communication within the Effects framework: you can find this very small sample program here.

The PacketLang EDSL

The PacketLang embedded DSL, first shown by Edwin Brady in this paper, provides a way of describing packet-level data, along with specifying constraints on it. The EDSL is specified using induction-recursion, meaning that subsequent parts of a packet specification may be determined by prior data. IdrisNet2 reimplements this for the latest version of Idris, and it’s now possible to use it with the verified bindings for TCP and UDP,  too.

At a high level, PacketLang provides a mechanism by which we may specify the structure of packets. For example, we could have a simple packet containing two strings:

simplePacket : PacketLang
simplePacket = do cstring
                  cstring
and a concrete instance of the packet:
simplePacketImpl : (mkTy simplePacket)
simplePacketImpl = ("hello" ## "world")

What’s happening here is that the mkTy function is used to translate the specification into concrete Idris types – in this case, a pair of strings. The ## notation is syntactic sugar for a dependent pair.

PacketLang allows several basic types of data to be specified: C-style null-terminated strings, strings of a given length, numbers representable by a given number of bits, and Boolean values. Additionally, there are control structures to allow lists of values, lists of values of a given length, a choice of specifications, if-style Boolean tests, and propositions on values. We’re only going to be using the basics for this, so I’ll skip the details, but if you’re interested check out the original paper or my BSc project report.

Putting it all together…

With all the ingredients, let’s get stuck in!

Setup

The overall architecture I’m using is a basic client-server one, although the only difference in practice is that the server calculates changes in the ball position and sends these off to the client.

The game state contains the width and height of the canvas, the positions of the paddles, and whether or not buttons are pressed, which signifies that a paddle should be updated. Additionally, we want to know whether the ball is currently attached to the paddle awaiting launching, whether we’re a client or server, and the address and port of the remote server.

record GameState : Type where
 MkGameState : 
 (pongWidth : Width) -> -- Canvas width
 (pongHeight : Height) -> -- Canvas height
 (pongBall : PongBall) ->
 (pongLeftPaddlePos : (Int, Int)) -> -- Position of the left paddle
 (pongRightPaddlePos : (Int, Int)) -> -- Position of the right paddle
 (pongIsUpPressed : Bool) -> -- Is up pressed? If so, decrease Y pos
 (pongIsDownPressed : Bool) -> -- Is down pressed? If so, increase Y pos
 (pongToLaunch : Bool) -> -- Has the launch button been pressed?
 (pongIsPaddleChanged : Bool) -> -- Has the direction of the paddle changed?
 (pongRemotePaddleUp : Bool) ->
 (pongRemotePaddleDown : Bool) ->
 (pongNetworkMode : PongNetworkMode) ->
 (pongRemoteAddr : SocketAddress) ->
 (pongRemotePort : Port) ->
 GameState
record PongBall : Type where
 MkPongBall : 
 (pongBallPos : (Int, Int)) ->
 (pongBallXVel : Int) -> -- X Velocity
 (pongBallYVel : Int) -> -- Y Velocity
 (pongBallStuck : Bool) -> -- Whether the ball is attached to a paddle or not
 (pongBallHitLeft : Bool) -> -- Whether the ball last hit the left paddle
 PongBall

Right, with that all done, we can begin to look at how everything fits together. The overall program requires all the effects to be used, so we can set them up and use them within the game loop. It therefore makes sense to define a type synonym, Pong, detailing all of the effects:

Pong : Type -> Type -> Type 
Pong s t = { [ SDL s
 , STATE GameState
 , STDIO
 , UDPCLIENT
 , PROCESS (Running GameMessage)] } Eff IO t

The Pong type is parameterised over two values: the state of the SDL effect (as some operations are only valid when this is initialised), and the return type.

After setting this all up, we can get the initialisation going. Running the effectual Pong program with an initial state, we then execute the pongMain routine. pongMain : Port -> Pong () () pongMain p = with Effects do st <- get initialise (pongWidth st) (pongHeight st) setupUDP p eventLoop quit

This starts off by getting the current state using the get operation which is part of the State effect. Secondly, we initialise the SDL effect using the width and height given in the state. Thirdly, we set up the UDP server, before entering the event loop. Finally, we clean up the open SDL resources. We also define another type synonym, PongRunning, which specifies that the SDL effect has been initialised.

The setupUDP function spawns a new thread with a UDP server. These are sent back to the main thread using the GameMessage data type—we’ll get to that in a minute or two. You’ll see here that we grab the ID of the current thread, so the network handler thread knows where to send the update messages. setupUDP : Port -> PongRunning () setupUDP p = with Effects do pid <- getPID spawn GameMessage (networkHandlerThread p pid) [(), ()]

Time to get onto the main game loop!

Game Loop

In the game loop, we firstly grab a copy of the state. Secondly, we check for any network events by checking whether the network thread has sent the main thread any messages. We then use the handleKeyEvents function from the SDL library to check whether any keys have been pressed or released, updating the relevant fields in the state if so.

The next thing to do is update the remote paddle position, based on whether the remote user has up or down held down.

After that, we update the local paddle position based on whether the current user pressed up or down, sending a packet to the remote peer if there have been any changes in the movement direction.

The final two things involve updating the ball position: in the case of the server, this means checking to see whether there has been any change in either X or Y velocity and if so, relaying this to the remote client. If not, then this means updating the local ball positions based on the X and Y velocities we have.

The final step is to draw the game, based on the current positions of the objects, using the draw function.

Each of these only use a subset of the available effects: handling the key events and updating the game state require the state effect, handling the network events requires the process and state effects, and so on. The sublists of effects are automatically checked, without any need for explicit lifting (which is nice :))

eventLoop : PongRunning ()
eventLoop = do
 st <- get
 handleNetworkEvents
 continue <- handleKeyEvents !poll
 updateRemotePaddlePos
 paddle_updated <- updateLocalPaddlePos
 when paddle_updated (sendPaddleUpdate >>= \_ => return ())
 if (isServer st) then serverEvents else updateBallPos
 draw
 when continue eventLoop

Most of this process is pretty mechanical, but it’s probably worth looking at the serverEvents and updateBallServer functions,  since they encode most of the game logic.

serverEvents : PongRunning ()
serverEvents = do
 ball_updated <- updateBallServer 
 when ball_updated (sendBallUpdate >>= \_ => return ())
updateBallServer : { [STATE GameState] } Eff IO Bool
updateBallServer = do
 requires_launching <- requiresLaunching
 when requires_launching launchBall
 paddle_collision <- checkPaddleCollisions
 lr_bounds <- checkLRBounds
 tb_bounds <- checkTBBounds
 updateBallPos -- Apply X and Y velocities to move the ball
 return $ requires_launching || paddle_collision || lr_bounds || tb_bounds

The purpose of these functions is to check for any collisions, and if so, update the ball velocities accordingly. Should a change in ball velocity occur (if, for example, the ball has been launched or it has hit a wall or a paddle), this is relayed to the client.

Communication

Communication is done over UDP, with communication between threads using the GameMessage data type.

Sending Updates

There are two types of packets we need to send: one is a paddle position update, and one is a ball position update. To this end, we make 3 PacketLang definitions: ballUpdate, paddleUpdate, and statusUpdate. The statusUpdate packet is simply a wrapper around the other two, differentiating the two types of packet using a Boolean flag.

ballUpdate : PacketLang
ballUpdate = with PacketLang do
 x <- bits 32
 y <- bits 32
 xv_neg <- bool -- True if X-vel negative
 x_vel <- bits 32
 yv_neg <- bool -- True if Y-vel negative
 y_vel <- bits 32
 bool -- Stuck to paddle?
 bool -- Last hit the left paddle
paddleUpdate : PacketLang
paddleUpdate = with PacketLang do
 bool -- Up pressed
 bool -- Down pressed
 bits 32 -- X
 bits 32 -- Y
statusUpdate : PacketLang
statusUpdate = with PacketLang do
 is_ball <- bool -- True if ball update, false if paddle
 p_if is_ball then ballUpdate else paddleUpdate

The data sent using these packet structures is fairly self-explanatory. The one small wart with this is that the bits construct only encodes positive numbers, so there’s an extra flag to state whether or not a number is negative. It’s really just an implementation detail though, not a massive limitation.

All that really remains to discuss is encoding, sending, and decoding the packets. Let’s have a look at sendPaddleUpdate, which sends a paddle update packet based on the current values in the game state.

sendPaddleUpdate : { [STATE GameState, UDPCLIENT] } Eff IO Bool
sendPaddleUpdate = do
 st <- get
 let sa = pongRemoteAddr st
 let p = pongRemotePort st
 let up_pressed = pongIsUpPressed st
 let down_pressed = pongIsDownPressed st
 case m_pckt up_pressed down_pressed !getLocalPaddlePos of
   Just pckt => do IdrisNet.UDP.UDPClient.udpWritePacket sa p statusUpdate pckt
                   return True
   Nothing => return False
 where m_pckt : Bool -> Bool -> (Int, Int) -> (Maybe (mkTy statusUpdate))
   m_pckt up_pressed down_pressed (x, y) = with Monad do 
   b_x <- mkBounded 32 x
   b_y <- mkBounded 32 y
   return (False ## up_pressed ## down_pressed ## b_x ## b_y)

The function requires two effects: the state, and the UDP client. After getting the required information from the state, we construct a statusUpdate packet instance by checking to see whether the X and Y positions fit inside 32 bits using the mkBounded function (mkBounded provides a Bounded instance, carrying a proof that the number fits within the given number of bits), and sequencing these together using the ## operator.

Finally, if this packet is constructed successfully, then it is sent using the udpWritePacket function. This function takes the remote address and port, the packet specification, and the concrete instance.

Receiving Updates

Receiving updates is done in our spawned network handler thread.

networkHandlerThread' : (mthread : ProcPID GameMessage) -> 
                        RunningProcessM GameMessage IO 
                          [UDPSERVER UDPBound, STDIO] 
                          [UDPSERVER (), STDIO] 
networkHandlerThread' pid = with Effects do
 UDPSuccess (_, Just (pckt, _)) <- IdrisNet.UDP.UDPServer.udpReadPacket statusUpdate 256
   | UDPSuccess (_, Nothing) => do putStr "Error decoding status packet\n"
                                   networkHandlerThread' pid
   | UDPFailure err => do IdrisNet.UDP.UDPServer.udpFinalise 
                          return ()
   | UDPRecoverableError err => do IdrisNet.UDP.UDPServer.udpClose 
                                   return ()
 let msg = mkMessage pckt
 sendMessage pid msg
 networkHandlerThread' pid

This function uses the udpReadPacket function to try and receive and decode a statusUpdate packet. If this is successful, then we use the mkMessage function to translate this into a GameMessage instance, and send this to the master thread using sendMessage. If not, then we handle the failure inline using the failure handling notation.

GameMessage and mkMessage are pretty simply defined as follows:

data GameMessage = UpdateRemotePaddle Bool Bool Int Int -- Up pressed, down pressed, x, y
 | UpdateRemoteBallPos PongBall
mkMessage : (mkTy statusUpdate) -> GameMessage
mkMessage (True ## x ## y ## xv_neg ## xv ## yv_neg ## yv ## stuck ## left) = 
 UpdateRemoteBallPos $ MkPongBall (val x, val y) xv' yv' stuck left
 where xv' = if xv_neg then ((val xv) * (-1)) else (val xv)
 yv' = if yv_neg then ((val yv) * (-1)) else (val yv)
mkMessage (False ## up ## down ## x ## y) = UpdateRemotePaddle up down (val x) (val y)

These basically unmarshal the data from the packet (the val function translates the Bounded representation of an integer to a simple Int type), translating it into a simpler form which may be sent to the main process. The final piece of the jigsaw is handling such a message in the handleNetworkEvents function called from the game loop.

handleNetworkEvents : { [STATE GameState, 
                         PROCESS (Running GameMessage)] } Eff IO ()
handleNetworkEvents = when !hasMessage (do
 st <- get
 case !recvMessage of
 (UpdateRemotePaddle r_up r_down x y) => 
   if (isServer st) then
     put ( record { pongRemotePaddleUp = r_up, 
                    pongRemotePaddleDown = r_down,
                    pongRightPaddlePos = (x, y) } st )
   else
     put ( record { pongRemotePaddleUp = r_up,
                    pongRemotePaddleDown = r_down, 
                    pongLeftPaddlePos = (x, y) } st )
 (UpdateRemoteBallPos ball) => put ( record { pongBall = ball } st ))

This program checks to see whether there is any message sent by the network thread using the hasMessage function, provided by the Process effect. If so, it is received using the recvMessage function, and the state is updated accordingly.

That’s all, folks!

That’s pretty much it! With all these pieces together, we have a working networked Pong game. Feel free to try it out yourselves, and indeed make your own games!

If you’re still here, thanks for reading. I hope you’ve seen how Idris can be used for networked applications, how Effects can be used to produce more modular programs, and have enjoyed at least some of the post.

I’d love to hear any comments or criticisms people have, as ever: by all means drop me an e-mail.