Has anyone managed to get their heads around dependently typed string diagrams? Trying to figure out what they might look like and it's hurting my brain! Might not help that I'm not super experienced at category theory… 😬
Conversation
Yeah I remember now seeing your tweet about it! Was contemplating asking if you'd got any further on it!
Quote Tweet
So the nightmare with "dependent string diagrams" is that the *topology* of a diagram can depend on values in it. I think the idea is that each possible topology goes in its own slice
This often happens in game theory, when the structure of the game depends on earlier choices
Show this thread
1
1
I'm cool with deferring the harder CT stuff to more experienced people - I'm more interested in experimenting with silly programming language implementations based on this kind of thing (but perhaps that's premature? 😅).
1
3
Since then I started playing around with branching string diagrams for game theory, running mostly with my gut feeling. I think these are like sigma types. When I try to figure out what I'm actually doing here, my brain melts for 2 whole different reasons
1
1
Oooh, are the left-pointing triangles sort of splitting the diagram into slices(?) - ie. depending on what is in the first element of the sigma type?
2
1
Oh no what is happening to me
1
3
thinking about how disjoint union (sum) types are special cases of dependent pair (sigma) types
1
1
Couldn’t help making a paper model!
1
5
14
Replying to
Yeah! I was wondering about those backwards diagrams 😅
I was also thinking about diagrams where the class wires affect the types of other wires, but I could be off the mark there:
Quote Tweet
Replying to
This is funky. I have no clue whether you could make this precise or not, I can believe both possibilities
1
2
Yeah, me neither! One thing that I don't think is captured here is evaluation... not sure if that is important. had some comments in that thread that suggested stuff along those lines.
1
2
Show replies