I think I might be using "irrelevance" where I mean "erasure"/"erasibility", or vice versa. Do those mean the same thing or is there a fine distinction?
What does "allowed to treat them as multiplicity 0" mean in practice? I thought lower mult.s give you strictly fewer options?
Conversation
I'm not an expert on either of these topics, but irrelevance as in "computational irrelevance" seems to be equivalent to "erasibility" to me. And I'm not aware of any kind of irrelevance that does not imply computational irrelevance.
1
2
Regarding multiplicity, yes, 0 gives you fewer options, OTOH lower multiplicity is of course desirable for better performance. We statically know that we do not need the "more options" for any proof value because of computational irrelevance, so we know they will always be erased
1
1
What is the dual of multiplicity 0 on a binder/parameter? ie. What does it mean to return something that can never be used?
2
Related:
Quote Tweet
@dorchard @buggymcbugfix 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?
Show this thread
1
1
ie. multiplicity 1 on the return type seems to be uniqueness typing (ie. the dual of linear typing)
1
Hmm is it? I see two possibilities (which I think are different): no more than 1 copy/alias of this exists (uniqueness typing), vs. the caller only gets 1 copy of it. And the latter seems more likely...
1
I want it to be the former :( - why does the latter seem more likely?
1
Well, that's just what it means elsewhere -- how many copies you get to use, not how many exist.
(There was something in the linear haskell paper wrt `forall a. (Foo -o a) -o a)` being an encoding of a linear value; maybe that gets you closer?)
1
yeah, in that thread I was just reading that linearity doesn't get you mutate in place semantics, which is what I really want :/
1
Replying to
What stops you from enforcing uniqueness for 1 rather than linearity? Something breaks; or just not clear how?
1
Also IIUC, "linearity" of an arg means "callee may only use it once, caller any number of times", and "uniqueness" is the reverse, "caller may only use it once, callee any number of times", but I think you'd want to restrict both sides? At least Rust works that way...
1
1
Show replies