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.
James Wood (Apr 09 2020 at 20:13):Henry Story said:
Re.linear logic, I have an idea in the back of my head that it is particularly appropriate for dealing with speech acts. (since many acts are unique. Eg. buying something is a unique act. buying it twice would get one two items not one.)
How does this compare to the ideas behind session types?
Henry Story (Apr 09 2020 at 20:17):Argh, session types are on my reading list too...
James Wood (Apr 09 2020 at 20:20):Any particular articles? Unless you have something specific in mind, Phil Wadler's paper is the one that normally gets recommended, and I think it's quite good.
Henry Story (Apr 09 2020 at 20:26):You mean this one by Wadler Propositions as Sessions? Actually I had been pointed to session types for protocols a few times, and was watching an video Two sides of the Same coin: Session Types and Game Semantics when I must have gotten somehow lost into reading more about dialogical reasoning. :-) Thanks for reminding me.
James Wood (Apr 09 2020 at 20:30):Yeah, that one. Though I don't know about this video, and if there's a paper associated with it, it sounds promising.
James Wood (Apr 09 2020 at 20:33):IIRC, Phil's paper is concerned with quite syntactic matters, so your mileage with it may vary.
James Wood (Apr 09 2020 at 20:34):Oh wait, was I there for this talk...? :rolling_on_the_floor_laughing:
Joe Moeller (Apr 09 2020 at 21:02):What's the basic idea behind the word "sessions" here?
James Wood (Apr 09 2020 at 21:11):I'm not really an expert, but I think “session” refers to a synchronous communication between two processes. Information is sent via the additive connectives – a process satisfying session type sends a bit and continues as either or (according to that bit), and dually, this bit can be received by a process satisfying session type , which branches on the bit it receives and continues in the relevant way. I can't remember what the multiplicative connectives do.
Gershom (Apr 09 2020 at 21:17):the "CS" motivation behind "session" is you think of it as wanting to encode the protocol for interaction between a client and server. So the mail client sends to the server HELO to initiate, but it may also send EHLO to initiate, which opens an "extended" protocol, after which more commands are available than otherwise. The server responds from a defined set of choices to each message, and at certain branch points either the client or server may choose from a number of different things to send next, and the things that may be sent next should be related to the things that were sent before in a specified way, etc.
So it is a very formalized notion of "each side" of a conversation, with the nice property that if you know only one side's protocol you can "flip" it (or negate it) and figure out the protocol on the other side, and given two such gadgets you can formally ensure they match up -- that the server has some branch for responding to every client request, etc.
Joe Moeller (Apr 09 2020 at 22:13):That makes sense, thanks.
Gershom (Apr 09 2020 at 22:15):can't believe i missed the opportunity to say "you put that type down, flip it and reverse it."
John Baez (Apr 09 2020 at 22:23):In case anyone didn't get that allusion:
Christian Williams (Apr 09 2020 at 23:39):This topic should be in #theory: type theory.