Allen's lambda syntax proposal

Mark S. Miller erights at
Mon Dec 8 08:36:11 PST 2008

On Mon, Dec 8, 2008 at 7:20 AM, Jon Zeppieri <jaz at> wrote:

> On Mon, Dec 8, 2008 at 4:01 AM, Yuh-Ruey Chen <maian330 at> 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
> exception.
> Non-termination is an effect, and it's notoriously immune to runtime
> checks.
> 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 <> <> 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 <>, 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...
URL: <>

More information about the Es-discuss mailing list