Allen's lambda syntax proposal
Mark S. Miller
erights at google.com
Mon Dec 8 08:36:11 PST 2008
On Mon, Dec 8, 2008 at 7:20 AM, Jon Zeppieri <jaz at bu.edu> wrote:
> On Mon, Dec 8, 2008 at 4:01 AM, Yuh-Ruey Chen <maian330 at gmail.com> wrote:
> > Breton Slivka wrote:
> >> 2) It would be really nice to have a callable value that was
> >> garaunteed not to have side effects.
> > This little comment got lost in the recent deluge of emails, but I too
> > would really like some mechanism to avoid or see if a function causes
> > side effects (and not just mutability).
> Without a static type system, there's very little you can do.
> Sure, you could abandon the proof requirement and turn it into an
> assertion, so that if F is annotated as "mutation-free" and if, at
> runtime, it tries to perform an assignment, an exception is thrown.
> But this doesn't work so well for other computational effects.
> Throwing an exception itself is an effect, and it would be pointless
> to throw an exception when your code illegally attempts... to throw an
> Non-termination is an effect, and it's notoriously immune to runtime
> I/O effects are possibly the most interesting from a practical
> perspective, but they're outside the scope of the ES standard.
E's auditors <http://www.erights.org/elang/kernel/auditors/> <
http://wiki.erights.org/wiki/Guard-based_auditing> are a mostly non-static
approach that can verify many properties, including side effects per se
including IO effects, but not including throws and non-termination. Joe-E's
similar, but non-extensible and static auditor system <
http://www.cs.berkeley.edu/~daw/papers/pure-ccs08.pdf>, has been used to
verify some nice purity properties.
I am not ready to propose any such thing for Harmony at this time.
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Es-discuss