Category Theory
Zulip Server
Archive

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.

Stream: theory: applied category theory

Topic: Sheaf models for permission systems

Reed Mullanix (Apr 01 2020 at 19:46):

Been thinking about sheaves a lot recently, and realized that they could be used potentially be used to model capability/permission systems for software systems. Does anyone have any papers/resources that explore this?

Jules Hedges (Apr 01 2020 at 19:50):

I feel like this sounds very faintly familiar, like I saw a talk about it 2 years ago or something. But maybe I just imagined it, or had a conversation about it in a pub

Fabrizio Genovese (Apr 01 2020 at 19:52):

Reed Mullanix said:

Been thinking about sheaves a lot recently, and realized that they could be used potentially be used to model capability/permission systems for software systems. Does anyone have any papers/resources that explore this?

What do you mean precisely with "permission system"?

Reed Mullanix (Apr 01 2020 at 19:55):

So for a very boring example, say you have some application where you have a bunch of actions that users can perform. However, we only want certain users to be able to perform certain actions.

Reed Mullanix (Apr 01 2020 at 19:59):

Let's call the ability to perform an action a "capability" (or "permission). We can then consider some topology over these capabilities, and we can form functors to Set that describe the sets of actions that we can take.

Reed Mullanix (Apr 01 2020 at 19:59):

Though now that I think of it, perhaps stacks may be a better fit here, but I have an extremely fuzzy understanding of them

sarahzrf (Apr 01 2020 at 23:57):

well, why are you going for sheaves?

sarahzrf (Apr 01 2020 at 23:58):

do you already have a reason for there to be a topology? do you think that "locality" is a relevant concern?

Fabrizio Genovese (Apr 02 2020 at 00:06):

There's naturally a topology on the actions if you arrange them in a graph or in a lattice, which seems very natural given the context. I'm more worried about the functorial part. The only meaningful way to carry actions into actions seems to be inclusion (Higher permission includes what lower permissions can do). But this makes the sheaf trivial.

Fabrizio Genovese (Apr 02 2020 at 00:06):

On the contrary, having a more complicated relationship on the actions may make the sheaf interpretation more difficult. Maybe you want a presheaf instead?

Fabrizio Genovese (Apr 02 2020 at 00:08):

I've thought about sheaves a lot as well, mainly for a similar but unrelated problem I'm investigating with @Matteo Capucci , and I convinced myself that sheaves really are everywhere and are one of the best things (if not the best) one can use in the compositional toolkit.

Bob Atkey (Apr 02 2020 at 13:12):

There's a recent draft by Neel Krishnaswami and @vikraman that models capabilities via a kind of fuzzy sets construction (https://www.cl.cam.ac.uk/~nk480/icfp20-cap-submission.pdf). Fuzzy sets are sets $X$ plus a "fuzzy membership" predicate $X \to [0,1]$. That paper replaces the interval $[0,1]$ with the opposite of the lattice of subsets of a set of capabilities. Such fuzzy sets are known to be a quasitopos, and are a subcategory of the category of sheaves on a complete Heyting algebra (https://www.sciencedirect.com/science/article/abs/pii/S0165011406005367).

vikraman (Apr 02 2020 at 14:12):

Fuzzy sets or weighted sets over a locale are monic sheaves over the locale, with the trivial Grothendieck topology. This observation is originally due to Michael Barr. I have a few generalisations of it to sheaves over quantales which can be used to build models of type theory with monads and comonads that track intensional resources. I was going to talk about this at SYCO 7 which was postponed.

Bob Atkey (Apr 02 2020 at 14:16):

Cool! Do you have any slides or antyhing?
One thing that occurred to me is that your category of "capability sets" is a sort of poset version of the category of containers; instead of $(S : \mathrm{Set},P : S \to \mathrm{Set})$ you have $(X : \mathrm{Set}, w : X \to \mathcal{P}(C))$. Several of the constructions look formally the same.

vikraman (Apr 02 2020 at 14:23):

Ah, I did not prepare slides since SYCO was postponed. :-P

Yes, I also noticed the similarity with containers, so I tried to work out if it makes sense to have a category-weighted set/object. However, it does not look as elegant as containers and I couldn't apply it to any semantics problems.

vikraman (Apr 02 2020 at 14:27):

I can also express it as a category of elements actually.

Bob Atkey (Apr 02 2020 at 14:38):

By category weighted, do you mean $(X, X \to \mathcal{C})$ for some other category, or $(X, X \to \mathrm{Cat})$?

Bob Atkey (Apr 02 2020 at 14:39):

These slides by David Spivak talk about a generalisation of containers to families of objects in categories over than $\mathrm{Set}$: http://www.math.ucr.edu/home/baez/ACTUCR2019/ACTUCR2019_spivak.pdf

vikraman (Apr 02 2020 at 14:57):

Yes $E = (X, X\rightarrow C)$ for some category $C$, and morphisms in $E$ come with families of morphisms in $C$. Then, $E$ has products/exponentials/pi-types etc. iff $C$ has ...

vikraman (Apr 02 2020 at 14:57):

Thanks, I'll take a look at Spivak's slides.

Bob Atkey (Apr 02 2020 at 15:17):

That's very cool. Did you look at the non-cartesian monoidal structures too?