(This is an update on my Ethereum Protocol Fellowship. More updates can be found here ).


As part of my fellowship at the Ethereum Foundatoin, I am modelling game theory using an aproach from category theory called Open Games. To do this, I am using the Open Game engine, which is still in development. To help other that might want to work with this engine, and aid further development, I have kept a list of questions I ran into, most of which have been answered by Philipp and Jules. These are not covered in the tutorial, so worth printing here:


Q: How should one read the type of an open game?

Let’s take the game from a previous update:


pieSharingGame pie = [opengame|

   inputs    :      ;
   feedback  :      ;

   :----------------------------:
   inputs    :      ;
   feedback  :      ;
   operation : dependentDecision "proposer" (const [0..pie]);
   outputs   : proposal ;
   returns   : pieSharingGamePayoff_proposer pie proposal reaction;

   inputs    : proposal ;
   feedback  :      ;
   operation : dependentDecision "responder" (const [Accept,Reject]);
   outputs   : reaction ;
   returns   : pieSharingGamePayoff_responder pie proposal reaction ;

   :----------------------------:

   outputs   :      ;
   returns   :      ;
   |]


This has the following type:


λ: :t pieSharingGame
pieSharingGame
  :: Double
     -> OpenGame
          StochasticStatefulOptic
          StochasticStatefulContext
          '[Kleisli Stochastic () Double,
            Kleisli Stochastic Double ResponderAction]
          '[[DiagnosticInfoBayesian () Double],
            [DiagnosticInfoBayesian
               Double ResponderAction]]
          ()
          ()
          ()
          ()


It’s a map from a Double (the size of the full pie) into an OpenGame. The OpenGame then has a complicated type. The first two lines (Stochastic…) can be ignored for now, let’s focus on the rest. It starts with a list with one element for each player in the game. Each element describes the type of that player’s strategy. For player 1, the proposer, that is Kleisli Stochastic () Double, because it is a map from the unit () to a pie size, i.e. a choice of a cut. The second player observes the offer and chooses to accept or not, so indeed has strategies of type Kleisli Stochastic Double ResponderAction. (Recall that a type Kleisli Stochastic a b can be seen as a map a -> Stochastic b) Then follows a list with diagnostic types for each player—not so interesting for now. Finally, we get four empty tuples, which correspond to the four dangling wires from the external game—in this case four empty wires, hence the empty tuples.


Q: How are the payoffs matched to the players?

It turns out there is a hidden ‘state’ that keeps track of how the payoffs get attributed to players. Usually, this happens through the returns wire, however, there is also a function addPayoffs that can directly add payoffs to the players from the operation field.


Q: The staking example and the model of the FTX crash are almost completely built from functions lifted to games. Doesn’t this negate the whole point of the engine?

This would be true if they are all deterministic functions. However, lifted stochastic maps can still be interesting. I believe this has something to do with Bayesian reasoning, although perhaps you would also need backward functions for this? I don’t really understand this yet.


Q: The staking example sets the returns field to 0 sometimes. Why do this instead of leaving it empty?

Even if you do not want to add a payoff to a player during that operation, it still needs to be set. Assuming that payoffs are an additive quantity, 0 is the neutral element that can always be added.


Q: Why is the feedback wire rarely used in the examples?

Since the category of open games has a map from a covariant output to a contravariant output (i.e. a cup), outputs can trivially be converted to feedback. It’s often easier to just send all information to the output, and use implicit cups by just setting the output variable as the returns from some other game.


Q: In a dependent decision that outputs, say, a tuple, how do you specify what is output and what is feedback?

This is apparently possible, but I don’t know how. In any case, this is not really necessary, since you can usually use implicit cups to change output into feedback.


Q: Why go through the effort of creating contexts? Couldn’t you just as well define a closure game by sandwiching the game you want to analyse between a point and a copoint, and analyse that closed game in a void context?

The two are indeed mathematically equivalent, however, creating contexts offers more flexibility. For example: say you have a complex model involving many games. You might want to analyse the system at different ‘levels’ of composition. You would need to create closure games for each level you want to analyse, which is terrible inefficient and redundant. Furthermore, you need to construct strategies for the point and copoint ‘players’, which is unnecessary work. This is what contexts solve.


Q: How do you construct a context?

A good trick to figure out the required type of a context for a game OpenGameFoo is by running


:t evaluate OpenGameFoo


Since evaluates expects a list of strategies and a context, this outputs the type of both of these. For example, in the case of the closed pieSharingGame:


λ: :t evaluate (pieSharingGame 10)
evaluate (pieSharingGame 10)
  :: List
       '[Kleisli Stochastic () Double,
         Kleisli Stochastic Double Examples.PieCutting.ResponderAction]
     -> StochasticStatefulContext () () () ()
     -> List
          '[[DiagnosticInfoBayesian () Double],
            [DiagnosticInfoBayesian
               Double Examples.PieCutting.ResponderAction]]


which shows that the context should be of the type StochasticStatefulContext () () () ().


Q: How is the order of the strategies in the final tuple determined?

The strategies should be in the order that the players’ decisions appear in the game. If the games are nested, then the order corresponds to the order in the completely denested game.


Finally, I came across a parser error when lists have only a single element lists. I raised an issue for this here