Linear Permissions

[chooseyourownlogic]

I wrote an unfortunately long pdf about linear logic and comonads. It might be interesting? It might solve a long-standing problem? Or it might just be a good way for me to procrastinate on my homework---only one way to find out!

Comments

[chrisamaphone]

i'm not able to prove cobind (as stated) with any of the box/! connectives you mentioned. what am i missing?

[chooseyourownlogic]

I think I remember talking about this with people on Twitter a while back---you can't actually prove it because the (W a -o b) function actually needs to exist at a different level, or something. So you can treat it like an inference rule:

W a -o b
--------
W a -o W b

and it works (and in fact, I do show this at the level of contextual transitions for the last system I present). Importantly, though, you can prove cojoin : W a -o W (W a) with any of them, which should be enough.

I'm not entirely sure what the rationale for this is, but it has something to do with how things are only functorial at a 'higher' level: so you don't have, say,

!A -o (A -o B) -o !B

but you *do* have

!A -o !(A -o B) -o !B

and similarly,

!A -o !(!A -o B) -o !B

The same things work for [].

[chrisamaphone]

yep - certainly if you make the ([]A -> B) argument be []'ed, it works, but i was curious why that doesn't correspond with the literature on comonads.

[chooseyourownlogic]

Yeah, I am also curious---I think the inference rule thing might answer it? But I'm not sure. Like I said, I asked this question on twitter a while ago; I think maybe William or Rob answered it (or you, but I guess not), so maybe they would know better? If they do, tell them to comment here so I can find out, too :P

[chrisamaphone]

i like the idea of having the "valid" and "true" judgments be represented by a 2-element preorder. it feels familiar, like something i've seen from jcreed.

i'm still not clear on how this constitutes a solution to permissions, though. what's your imagined encoding of "with permission p, a -o b"? does the permission become a worldy-resource?

[chooseyourownlogic]

Oh, really? I don't suppose you have a link to it or something? My only problem with them is that they aren't, um, particularly well-behaved; they don't seem to interact with tensor at all (at least, not by default), they're not associative, there's no unit (you could add one, but it would remove the nice property that you can't prove a box without a box), etc. This is also why I was asking about the comonadic version of strong monads on twitter.

I think that would be ([p]a) -o b.

[chrisamaphone]

i don't see anything in your pdf with that ([p]) syntax?

[chooseyourownlogic]

Oh, sorry, that's because I just made it up :P I don't think I used syntax for anything but unary box in the pdf? But I've been thinking of it as either "A [] B" (for the full binary case) or "[p]B" or "[]_p B" (for box indexed by some restricted universe of permissions).

So if you just wanted to write a function that morally has type a -o b, but with elevated permissions, you'd write ([]a) -o b to indicate that you need the extra privilege to get into the function.

[chooseyourownlogic]

I suppose it could also be something like []1 -o a -o b; I don't know if those should be equivalent or have different meanings or what, though that's kind of how I've been thinking of the OI comonad. That kind of feels like a weakness of the model, though. In the original presentation, the type OI a meant a computation of type a that depends on state, so you'd use counit to actually force the computation and make all the effects happen. Maybe that's still a valid interpretation here; I'm not sure. I know that if you can get away with just using []1 everywhere, it would feel like a deficiency in the logic.

[chrisamaphone]

well, they're modal operators in the kripke semantics sense, not in the resource semantics sense -- they form a preorder, not a monoid :)

[chooseyourownlogic]

but I want my binary logical connectives to be monoids D:

[chooseyourownlogic]

Er, and I'm not sure what you mean by a "worldly resource"? The cool thing is that you can write (persistent, or maybe privileged? dunno, it depends on my answer to your previous question, I guess, and I'm still not 100% on that) functions with that signature and not worry about duplicating the permission, since cobind does that for you! Or at least, that's the goal.

[chrisamaphone]

"worldy", not "worldly" :) i just meant "resource semantics resource" as opposed to "linear logic resource".

[chooseyourownlogic]

Oh, heh. If you're restricting it (so not the fully "dependent" case) to some set of permissions p, then yeah, kind of. Of course, the way I'm thinking of this isn't a straight-up resource semantics any more (I don't think), so I'm not sure it works quite like that.