On Tue, Dec 23, 2014 at 4:00 PM, Jonathan S. Shapiro <[email protected]> wrote: > On Tue, Dec 23, 2014 at 3:45 PM, Geoffrey Irving <[email protected]> wrote: >> >> On Tue, Dec 23, 2014 at 3:24 PM, Jonathan S. Shapiro <[email protected]> >> wrote: >> > On Tue, Dec 23, 2014 at 12:25 PM, Geoffrey Irving <[email protected]> >> > wrote: > > >> >> >> Not sure if this is the right time to >> >> discuss it, but the canonical example would be: will the effect system >> >> be able to implement a lazy data structure that seems pure from the >> >> outside? Feel free to ignore/table that question. >> > >> > Since BitC isn't a lazy language, I really doubt it. :-) >> >> That's why the question is whether the user can *implement* a lazy >> structure on top of the language... > > > Umm. First, I don't know that this rises to the level of the effect system. > The underlying argument here would be that you don't really care what the > actual value is until the first time you reference it, so this is getting > viewed as a form of lazy initialization. Let's further assume the > restriction that the generator function is pure, (in BitC this still permits > internally imperative behavior so long as the wrong things do not escape). > > Under these conditions, I *think* we can tell a story that lazy variables > can be viewed as pure. What we're going to lose by this story is the > termination argument for inductions. > > We can also allow the generator to emit a seed for the next call to the > generator. So, for example, a PRNG could be done this way. > > The really tricky question is whether the generator can consult and/or > update mutable cells during its computation phase, as would be necessary for > an RNG. That would introduce a very curious class of data structures that > are pure but not deterministic. > > All that being said, I have no plans at the moment to introduce lazy > evaluation into BitC. I'm not opposed. It's just a complication I don't want > to deal with right now. > >> >> Actually, I probably do know that it *is* hopeless: establishing >> purity requires checking a fairly complicated idempotency property. >> Alas. > > > I don't think so. The minute you introduced the caching, you resolved the > idempotence problem.
I think we're still talking about slightly different things, but I agree that it's not worth much analysis at this point. I think the situation is that 1. If we have support for lazy initialization in the language, the effect system can easily understand it and treat appropriate lazy code as pure. 2. If the language has no support for lazy initialization, the effect system won't notice that the typical idioms programmers use to implement laziness on top of mutability happen to produce pure interfaces. I was referring to (2). Geoffrey _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
