Jason (jcreed) wrote,
Jason
jcreed

Every once in a while this last week I keep going back to this email that Frank had cc'ed me on along with a bunch of other people, about some recent thoughts he had on session types and focusing and stuff. It reminds me that I never really understood session types hardly at all, since Frank and Luís's big paper on the Curry-Howardizing of them was from 2010, after I'd already left pittsburgh for philadelphier pastures.

Trying to digest that earlier paper now, I still have two big questions I don't know how to answer well, which are basically

(a) what happens with classical logic instead of intuitionistic?
(b) what happens with a symmetric tensor/lollipop instead of asymmetric?

As for (a), is the answer that standard session type systems connected to classical logic? Or no logic at all? I have no idea. All I know is it appears perfectly easy to start with [Concur10] and simply drop the requirement that the right-hand side of the sequent always has cardinality 1. I can make up some rules for par, I can prove classical linear logic shibboleths like (A ⊕ B)00 ⊸ A00 ⊕ B00 (where X0 means X ⊸ 0) like it's no big deal, and I get what seems to me to be a reasonable-looking process expression --- but maybe it lacks some important session-types-y property that I'm not familiar with.

For (b) I mean instead of rules like
Δ, y : A, x : B ⊢ P :: T
----------------------------⊗L
Δ, x : A ⊗ B ⊢ x(y).P :: T


Δ2 ⊢ Q :: y : A
Δ1 ⊢ P :: x : B
----------------------------⊗R
Δ1, Δ2 ⊢ (νy)x⟨y⟩.(P|Q) :: x : A ⊗ B

you could have rules like
Δ, y : A, z : B ⊢ P :: T
----------------------------⊗L
Δ, x : A ⊗ B ⊢ x(y,z).P :: T


Δ2 ⊢ Q :: y : A
Δ1 ⊢ P :: z : B
----------------------------⊗R
Δ1, Δ2 ⊢ (νy)(νz)x⟨y,z⟩.(P|Q) :: x : A ⊗ B

Now this requires having a primitive notion of sending (and receiving) a pair of channel names along a channel, but the treatment of additive disjunction and conjunction already required postulating the ability to perform inls and inrs and case operations on channels, so I think that's not objectionable.

what this does though is make x into not really a channel that gets reused at a different type at a later time during the session, but rather something that gets assigned a value once and only once. I think you can go farther and make all the session-type rules like this (observing that the shifts in the focusing treatment in Frank's recent note already have this property) so that it ceases to be a system of (nontrivial) channels at all, but something more like futures --- which I guess is kind of another way of viewing channels that only ever transmit one value, anyhow.

I wonder if this observation has any value, or whether on the other hand I might just recapitulating the history of session type research in reverse, by stripping away everything people actually like about them :P
Tags: math
Subscribe
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 10 comments