Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.


Stream: event: ACT20

Topic: July 8: Jules Hedges et al.'s talk


view this post on Zulip Paolo Perrone (Jul 02 2020 at 02:10):

Hello all! This is the thread of discussion for the talk of Jules Hedges and Philipp Zahn, "Open games in practice".
Date and time: Wednesday July 8, 12:35 UTC.
Zoom meeting: https://mit.zoom.us/j/7055345747
YouTube live stream: https://www.youtube.com/watch?v=AaaoUxUx-SQ&list=PLCOXjXDLt3pZDHGYOIqtg1m1lLOURjl1Q

view this post on Zulip Jules Hedges (Jul 08 2020 at 11:22):

Slides: https://obsoletewallstreet.files.wordpress.com/2020/07/open_games_in_practice.pdf

view this post on Zulip Paolo Perrone (Jul 08 2020 at 12:25):

10 minutes!

view this post on Zulip Juan Ferrer Meleiro (Jul 08 2020 at 13:03):

Hi!

view this post on Zulip Juan Ferrer Meleiro (Jul 08 2020 at 13:03):

So, to elaborate on my remark

view this post on Zulip Juan Ferrer Meleiro (Jul 08 2020 at 13:03):

I wasn't event talking about automation

view this post on Zulip Juan Ferrer Meleiro (Jul 08 2020 at 13:04):

Just inverting the logic

view this post on Zulip Jules Hedges (Jul 08 2020 at 13:05):

I was just scanning through the chat when zoom suddenly closed. So if anyone asked a question there, please ask it again here

view this post on Zulip Juan Ferrer Meleiro (Jul 08 2020 at 13:05):

Instead of specifying moves and utilities to get a equilibrium-evaluating function, specify desired equilibrium states and get a moves-and-utility evaluating function

view this post on Zulip Jules Hedges (Jul 08 2020 at 13:05):

Or if anyone can recover the zoom chat and dump it here?

view this post on Zulip Juan Ferrer Meleiro (Jul 08 2020 at 13:05):

Does that make sense?

view this post on Zulip Jules Hedges (Jul 08 2020 at 13:05):

Yes, I see. I'm not sure whether this is possible, I need to think about this a bit

view this post on Zulip Jules Hedges (Jul 08 2020 at 13:06):

This would be "compositional mechanism design" rather than "compositional game theory"

view this post on Zulip David Jaz (Jul 08 2020 at 13:06):

Jules do you have a repository for your DSL?

view this post on Zulip Juan Ferrer Meleiro (Jul 08 2020 at 13:06):

Yeah, I guess

view this post on Zulip David Jaz (Jul 08 2020 at 13:07):

Jules Hedges said:

This would be "compositional mechanism design" rather than "compositional game theory"

I'm not sure the field is big enough to split this hair yet :p

view this post on Zulip Juan Ferrer Meleiro (Jul 08 2020 at 13:07):

I'm not really versed in either, so I couldn't tell.how hard it would be

view this post on Zulip Jules Hedges (Jul 08 2020 at 13:08):

David Jaz said:

Jules do you have a repository for your DSL?

Here: https://github.com/jules-hedges/open-games-hs but the actual syntax I used in the talk isn't written down anywhere yet, so far it exists only in my head. The abstract syntax and its compiler can be found in /src/Preprocessor

view this post on Zulip Abel Jansma (Jul 08 2020 at 13:08):

Hi! That was great. Just as a follow-up on Aleks' question on what kinds of things this can tell you: You mentioned that economists really like this vcg auction for the incentives it induces. Is there already a way in which the DSL can show this, and how it's different from a normal auction where the winner pays the price they bid?

view this post on Zulip David Jaz (Jul 08 2020 at 13:08):

Jules Hedges said:

David Jaz said:

Jules do you have a repository for your DSL?

Here: https://github.com/jules-hedges/open-games-hs but the actual syntax I used in the talk isn't written down anywhere yet, so far it exists only in my head. The abstract syntax and its compiler can be found in /src/Preprocessor

Is this idea to extend arrow do notation with the payout functions?

view this post on Zulip David Jaz (Jul 08 2020 at 13:08):

Thanks!

view this post on Zulip Juan Ferrer Meleiro (Jul 08 2020 at 13:08):

“Code is the best documentation”

view this post on Zulip Jules Hedges (Jul 08 2020 at 13:09):

And here is the code for the talk specifically (warning: very messy, maybe not fit for human consumption yet): https://github.com/jules-hedges/open-games-hs/blob/permitSale/src/OpenGames/Examples/PermitSale/PermitSale.hs

view this post on Zulip Jules Hedges (Jul 08 2020 at 13:10):

David Jaz said:

Is this idea to extend arrow do notation with the payout functions?

Yes, I forgot to mention that the syntax is closely based on haskell's arrow-notation, modified to include the contravariant parts

view this post on Zulip Jules Hedges (Jul 08 2020 at 13:12):

Abel Jansma said:

Hi! That was great. Just as a follow-up on Aleks' question on what kinds of things this can tell you: You mentioned that economists really like this vcg auction for the incentives it induces. Is there already a way in which the DSL can show this, and how it's different from a normal auction where the winner pays the price they bid?

So my guess is that this kind of thing can't be shown by the representation. I normally think about this in terms of string diagrams, which can draw pictures of games but can't talk about their properties much (the language is very, very incomplete in the logical sense). If you add a 3rd dimension to the diagrams you can make some progress talking about properties of games. I doubt there's a practical way to do that in the textual representation

view this post on Zulip Jules Hedges (Jul 08 2020 at 13:16):

I'm going to have lunch now, if there's any more questions I'll get back to them in a bit

view this post on Zulip Jules Hedges (Jul 08 2020 at 13:18):

Oh, I just remembered I saw Viktor's comment disagreeing with me saying the equilibrium analysis isn't interesting to category theorists. This is true. For example, there's a homotopy theory of Nash equilibria. There's probably a deep rabbit hole hooking that up to open games

view this post on Zulip Philipp Zahn (Jul 08 2020 at 13:20):

Abel Jansma said:

Hi! That was great. Just as a follow-up on Aleks' question on what kinds of things this can tell you: You mentioned that economists really like this vcg auction for the incentives it induces. Is there already a way in which the DSL can show this, and how it's different from a normal auction where the winner pays the price they bid?

Maybe to add some context: Jules was effectively using a second price auction. In the particular situation we are looking at (2 players, just one "object" to be auctioned) this is an instantiation of the VCG mechanism. The latter is more general and can be used in different allocation problems (for instance public goods).

We could have used what you describe, a first price auction. In the scenario we consider, the first price auction can be shown to be "equivalent" to the second price auction. The difference is in the bidding strategies. In the second price auction, each player (in equilibrium) bids his private evaluation. In the first price auction you bid less. (Another difference is that VCG can be analyzed with a different notion of equilibrium)

view this post on Zulip Haskell (Jul 08 2020 at 13:21):

+1 on the "compositional mechanism design" question

I asked a similar(?) question a few weeks ago on the practice:economics stream, (although it's perhaps even more naive and confused) which I hope it's okay to paste here:

Hi, does anyone know of work on what might be called "compositional mechanism design"? AFAIK, you can't perform arbitrary computations on elicited truth values if the computations have effects, because that would disrupt the mechanism.

It would be great to be able to elicit truth valuations and treat them like ordinary inputs in programming and string them to outputs without having to worry about agents backpropagating on the program and hijacking it to get the personally desired outcome.

view this post on Zulip Abel Jansma (Jul 08 2020 at 13:24):

Jules Hedges said:

So my guess is that this kind of thing can't be shown by the representation. I normally think about this in terms of string diagrams, which can draw pictures of games but can't talk about their properties much (the language is very, very incomplete in the logical sense). If you add a 3rd dimension to the diagrams you can make some progress talking about properties of games. I doubt there's a practical way to do that in the textual representation
````

Right, that makes sense. Thanks!

view this post on Zulip Abel Jansma (Jul 08 2020 at 13:28):

Philipp Zahn said:

Abel Jansma said:

Hi! That was great. Just as a follow-up on Aleks' question on what kinds of things this can tell you: You mentioned that economists really like this vcg auction for the incentives it induces. Is there already a way in which the DSL can show this, and how it's different from a normal auction where the winner pays the price they bid?

Maybe to add some context: Jules was effectively using a second price auction. In the particular situation we are looking at (2 players, just one "object" to be auctioned) this is an instantiation of the VCG mechanism. The latter is more general and can be used in different allocation problems (for instance public goods).

We could have used what you describe, a first price auction. In the scenario we consider, the first price auction can be shown to be "equivalent" to the second price auction. The difference is in the bidding strategies. In the second price auction, each player (in equilibrium) bids his private evaluation. In the first price auction you bid less. (Another difference is that VCG can be analyzed with a different notion of equilibrium)

Ok that's actually very interesting, to be able to show these equivalences is kind of what I was getting at.

view this post on Zulip Philipp Zahn (Jul 08 2020 at 13:30):

The result is known as "Revenue equivalence theorem": a certain class of auctions will produce the same expected revenue. Goes back to Myerson.

view this post on Zulip Philipp Zahn (Jul 08 2020 at 13:33):

Haskell said:

+1 on the "compositional mechanism design" question

I asked a similar(?) question a few weeks ago on the practice:economics stream, (although it's perhaps even more naive and confused) which I hope it's okay to paste here:

Hi, does anyone know of work on what might be called "compositional mechanism design"? AFAIK, you can't perform arbitrary computations on elicited truth values if the computations have effects, because that would disrupt the mechanism.

It would be great to be able to elicit truth valuations and treat them like ordinary inputs in programming and string them to outputs without having to worry about agents backpropagating on the program and hijacking it to get the personally desired outcome.

I am not aware of something like that. At least not similar to compositional game theory.

view this post on Zulip Philipp Zahn (Jul 08 2020 at 13:35):

As concrete equilibria do not compose, there are natural barriers to compositional mechanism design where the well-behavedness of composite equilibria would be key I guess

view this post on Zulip Philipp Zahn (Jul 08 2020 at 13:36):

(I am, of course, restricting myself to what is narrowly defined as mechanism design in economics). It seems like you have something more general/ different in mind.

view this post on Zulip Paolo Perrone (Jul 08 2020 at 14:42):

Jules Hedges said:

Or if anyone can recover the zoom chat and dump it here?

Here's the chat, for those who are interested: Wednesday-I.txt

view this post on Zulip Jules Hedges (Jul 08 2020 at 14:48):

04:24:02 David Jaz: How does this dsl differ from arrow do notation, other than the missing “prop”?
It adds the contravariant part. This is to teleological categories as arrow notation is to monoidal categories, where "teleological categories" is the thing I invented that have the property that the category of optics is the free one on a monoidal category

view this post on Zulip Jules Hedges (Jul 08 2020 at 14:53):

04:19:26 Juan Meleiro: From listening to you at previous times, I had the impression you already had a working diagram interpreter
04:24:10 Viktor Winschel: Statebox has a text-to-string-diagram rendering code called KD editor which produces string diagrams but also Arrow-Haskell code. This might be a visualisation tool for otherwise textual specification of games. However this code might still lacks (not sure) a covariant arrow one needs for the coutility direction of arrows in open games.
Yes, I had to skip talking about that for time. We also hooked a branch of the Statebox diagram editor (which is implemented in javascript) so it generates haskell code for open games. There are 2 problems with that. One is that I can't hack on it, just because I don't have the code and I don't know javascript anyway. The other is something I wanted to mention but didn't have time. For bigger examples, this text-based notation with named wires starts to actually feel more convenient than string diagrams. You often end up making lots of copies and that can get quite messy in a string diagram with lots of comonoids and braiding. In the textual notation that's implicit, you just refer to the same name multiple times, and behind the scenes the compiler generates all the copy nodes

view this post on Zulip Jules Hedges (Jul 08 2020 at 14:55):

04:32:10 Viktor Winschel: I doubt that it is true that equilibrium analysis is economics and not interesting for CT. after all we might use algebraic geometry for example for analysing equilibria defined in polynomials. Actually we do that in economics already with homotopy continuation theory in “computational/numerical economics”.
Yes, agreed

view this post on Zulip Jules Hedges (Jul 08 2020 at 14:57):

04:32:36 Elena Di Lavore: it's not going to be more efficient than a global computation
The one possible exception is if you have a lot of pre-computed stuff solutions for your reusable components. And even that I think is unlikely

view this post on Zulip Jules Hedges (Jul 08 2020 at 14:58):

04:36:12 Matthew Di Meglio: The DSL looks very similar to Haskell do-notation, what do you get in the DSL that you couldn’t get from do-notation? Could this be used as a language for building string diagrams, say for typesetting purposes?
Yes.... I wonder if you could build an Arrow instance in haskell that generates diagrams (obviously using haskell's Diagrams package, which looks extremely nice). Hm, an interesting question

view this post on Zulip Erik Post (Jul 08 2020 at 16:15):

small correction re Statebox's kdmoncat string diagram editor (https://edit.statebox.cloud): although it is indeed still closed source, it's written in PureScript rather than Javascript, which, happily, is a more or lesss like a cleaner (and strict) Haskell

view this post on Zulip Paolo Perrone (Jul 08 2020 at 17:35):

Video here:
https://www.youtube.com/watch?v=b3aBFUrCpuw&list=PLCOXjXDLt3pYot9VNdLlZqGajHyZUywdI

view this post on Zulip Jules Hedges (Jul 09 2020 at 15:21):

Remembered that I promised a blog post link explaining the shenanigans with the state monad. In case anyone cares, this is it: https://julesh.com/2020/05/17/open-games-with-stateful-payoffs/ (this is the non-probabilistic version; the probabalistic variant in the talk is the one that was described as future work at the bottom of that post)

view this post on Zulip Sophie El Agami (Jul 14 2020 at 23:25):

Paolo Perrone said:

Jules Hedges said:

Or if anyone can recover the zoom chat and dump it here?

Here's the chat, for those who are interested: Wednesday-I.txt

Are the other zoom chat files somewhere? :grimacing:

view this post on Zulip Paolo Perrone (Jul 15 2020 at 01:14):

Sophie El Agami said:

Paolo Perrone said:

Jules Hedges said:

Or if anyone can recover the zoom chat and dump it here?

Here's the chat, for those who are interested: Wednesday-I.txt

Are the other zoom chat files somewhere? :grimacing:

I can post them on request.