On Tue, Dec 23, 2014 at 9:00 PM, Matt Oliveri <[email protected]> wrote: > 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?
The general case of this would pretty much have to wait for a future language with fully dependent types. In the near term, I don't see any solution other than having three levels of purity: 1. Impure. 2. Trust us, it's pure. 3. The compiler says it's pure. The distinction between (1) and (2) is purely for error/warning purposes, not soundness. Not sure if the existence of (2) helps much for the target applications, though it certainly would for the kind of code I'm writing right now (compiler-ish code with a lot of complicated manually written laziness). Geoffrey _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
