Modeling Purity as an effect system.md

gistfile1.md

Mapping from a more formal effect system to ours:

• Let fn:E() be a function with effects E
• Assume an effect lattice: pure -> impure -> unsafe
• fn foo(...) declares a function with effects impure
• pure fn foo() declares a functon with effects defined as follows: - let each argument of closure type have an effect variable: x: fn:X() - the effect of foo() is sum(X for all X) - if no closure arguments, the effect is pure
• calling a function with type fn:X() has the effect X

Therefore, when I write:

pure fn each(v: [T], x: fn(&T)) {
    while i < len(v) {
        x(v[i]);
    }
}

this is expanded to something like

fn each:X(v: [T], x: fn:X(&T)) {
    while i < len(v) {
        x(v[i]); // has effect X
    }
}

when I write:

pure fn other(v: [T], y: fn(*T)) {
    each(v, |e| {
        y(e)
    }
}

The type of the each(v, ...) must be fn:Y.
Therefore, the type of the closure is fn:Y(T). So it can only invoke y, not some other closure it may receive as argument.