chris martens (they/them) on Nostr: i’m not going to bother fishing out my last controversial post on the subject of ...
i’m not going to bother fishing out my last controversial post on the subject of whether “linear types” are a thing, but i do want to point out a related puzzle:
(1) “x is linear” can mean: “x is an assumption that must be used exactly once”
(2) “M is linear” can mean: “M is a term that uses all of its assumptions exactly once”
(or substitute your favorite usage restriction for “exactly once”)
and these notions are somehow dual(?) in a way i don’t yet understand
(1) “x is linear” can mean: “x is an assumption that must be used exactly once”
(2) “M is linear” can mean: “M is a term that uses all of its assumptions exactly once”
(or substitute your favorite usage restriction for “exactly once”)
and these notions are somehow dual(?) in a way i don’t yet understand