On Tue, Dec 23, 2014 at 7:29 PM, Geoffrey Irving <[email protected]> wrote: > 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. ... >>> >>> 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).
I don't know if this is what Geoffrey meant, but it made me think of a (possibly equal) question: Will there be a safe (not trusting the programmer) way to recognize benign effects as pure? This is hard. And if you can't do it, impure just sort of spreads all over the code, even if it's benign, making the effect system into noise. I hear this is a case where Haskell users use an escape hatch. (UnsafePerformIO, or something.) I don't think trying to bake all benign effects into the language implementation works. For starters, it's potentially worrisome to potential BitC users that a systems-y thing like caching would have to be baked into the language to work right. These are the kinds of things you should be able to write (and then use) /in/ a systems language! But worse, the general-purpose sorts of caching that you might bake in, like memoization, aren't everything. What about union/find trees and splay trees? How do you convince BitC that union/find trees with path compression are (can be) immutable data structures? _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
