Conversation

Oct 4, 2018

ie. multiplicity 1 on the return type seems to be uniqueness typing (ie. the dual of linear typing)

Oct 4, 2018

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...

Oct 4, 2018

I want it to be the former :( - why does the latter seem more likely?

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?)

yeah, in that thread I was just reading that linearity doesn't get you mutate in place semantics, which is what I really want :/

hence me wanty uniqueness as well

What stops you from enforcing uniqueness for 1 rather than linearity? Something breaks; or just not clear how?

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...

8:48 AM · Oct 5, 2018Twitter for iPhone

Yes, this is what I’m talking about 😅

Replying to

and

First read about the duality a while back in this link: twitter.com/buggymcbugfix/ - which lead me toasking poor

@buggymcbugfix

about it, which lead to him sending me the link. 😂

Quote Tweet

vilem

@buggymcbugfix

· Sep 18, 2018

Replying to @buggymcbugfix @brendanzab and @dorchard

PS: there is a simple explanation of uniqueness vs linearity here: edsko.net/2017/01/08/lin

Replying to

and

I am looking at this sort of stuff at the moment. I haven’t forgotten you...