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? 😅).
Conversation
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
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
1
1
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
Might have to do some more complicated things that need to be reduced to see if anything starts to break down. 🤔