hey, I’m curious what the 1 multiplicity behaves like in the effect position in Granule. Would that be equivalent to uniqueness? Ie. vs. the coeffect position which would be linearity?
Conversation
Do you mean what a type like `a <1>` vs `a |1|` means?
1
I think so? 😅
1
That doesn't mean anything in Granule at the moment.
Whether the multiplicity being an effect vs coeffect (i.e. grading on a monad vs comonad) has anything to do with linearity vs uniqueness is a great question. I need to think about this one a bit. Let me know if you find out!
1
1
PS: there is a simple explanation of uniqueness vs linearity here: edsko.net/2017/01/08/lin
1
2
Yeah, that's the blog post that originally got me thinking about it a while back, when they were mentioning that uniqueness typing was the dual of linear typing. Alas I don't really have a good enough grasp on the mathematics yet to do much with that yet.
1
1
And likewise, let me know if you have any thoughts/findings on this! Seems to be in the realm of adjacent possibility, so either: somebody is already thinking about this, or somebody is working on it/has done something already!
1
1
I'm also very interested in how effects/coeffects align with hoare/separation logic. It seems so similar, at least with my naive reading of it! I think I have a half-written email to sitting in my drafts that I never got around to finishing! 🤦♂️