hax more anii

So the lifetime of any datastructure can be separated into linear and parallel intervals, i.e. refcount 1 and refcount more than 1. On the linear lifetime segments, the data structure may be modified in-place to save both CPU cycles and memory; while on the parallel segments it better be immutable to make parallel execution simple and correct by construction.

Linear types (affine types, uniquness types, whatever) allow enforcing the linear intervals and make destructive update of the otherwise immutable structure acceptable.

Without linear types, you cannot have free lunch. Either you make everything immutable to pander to concurrency but lose speed and memory (and "purely functional data structures" are slow, damnit); or you stay in mutable-land and end up in a hell of data races and indetermination with its hard to reproduce but still quality-killing bugs.

But with linear types you can have your free lunch.

bampu pantsu

The Ecumenical Church of Linear Types

And now they're trying to unify linear types with dependent types. That's some sick shit right there, bro:

http://www.cs.bham.ac.uk/~krishnan/dlnl-paper.pdf

>>4
neelk please go