On Tue, Jul 22, 2014 at 7:52 AM, Jonathan S. Shapiro <[email protected]> wrote:
> On Mon, Jul 21, 2014 at 10:45 PM, Raoul Duke <[email protected]> wrote: > >> > Fair enough. But in this case the impediment is well-motivated and >> > insurmountable. Real programs require joins. Linear types do not permit >> > joins. >> >> (i'll hope to go really read and learn enough about types to know how >> to parse that, since google didn't tell me what "joins" are in this >> context, so i can learn if linear typing is therefore silly in e.g. >> ats :-) >> > > Sorry. Let me try to give you a sketch. > > Linear types work very well when you have a sequence of actions. They tend > to break down when you have alternative paths. You need to have one > "definitive" reference at all points, but the "fork" at the if/then/else > cause two to exist. And then at the bottom there is a join after the > if/then/else when the linear item returns to the unconditional control > path. > Do safe sum types make this situation better? An ability to express Maybe<LinearBuffer<T>> lets you use LinearBuffer<T> with dynamic checking in ambiguous control flow situations where the type checker couldn't prove single linear transfer. I think that C++11's std::unique_ptr is conceptually Maybe<LinearPointer<T>>, which actually seems to be very usable in the wild. std::unique_ptr<int> return_linear_int(...) { std::unique_ptr<int> ret; if (...) { ret.reset(std::move( one_source_of_linear_result() )); // ... } else if (...) { ret.reset( ... ); } // .. // .. return ret; }
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
