[Proposal] Generics/macros in Leo

[howardwu]

💥 Proposal

To support functionality, such as bounded recursion, and generalized algorithms, I propose adding the following notation in Leo for generics/macros:

function double[i](sum: u32) -> u32 {
    return double[i-1](sum + sum)
}

function main() -> u32 {
    return double[5](1)
}

[Protryon]

It was casually discussed we use this syntax instead:

function double(const count: u32, sum: u32) -> u32 {
    if count > 1 {
        return double(count - 1, sum + sum)
    } else {
        return sum + sum;
    }
}

function main() -> u32 {
    return double(5, 1)
}

Which seems more general purpose, and is already supported syntax.

On top of that, I have found an issue with input-based branched calling of recursion. I.e.

function double(const count: u32, sum: u32) -> u32 {
    if count > 1 && sum < 30 {
        return double(count - 1, sum + sum)
    } else {
        return sum + sum;
    }
}

function main() -> u32 {
    return double(5, 1)
}

This makes the recursion count depend on runtime data not as a function of what we are recursing on, but whether we call the recursive function or not. To deal with this issue, the following semantic constraints are proposed:

• All recursive calls cannot be within branches that depend on runtime variables. This includes cutting across the call tree, i.e. A -> B -> C -> A.
• As a result, some weird/confusing error messages

This should close this hole, and provide a safe compile-time recursion bound that is based on concrete semantics.

An alternative is runtime bounds checking, but that seems like a bad approach.

[acoglio]

The proposed (and already supported) syntax seems appropriate.

I'm expecting that the inlining of bounded recursion will take place alongside the other "flattening" transformations -- loop unrolling, constant propagation/folding, etc. If a recursion is const-bounded, the inlining should terminate at compile time, but we need to decide how to handle the other cases, such as

function forever(const n: u32) {
    forever(n);
}

function main() {
    forever(5);
}

An approach is to allow only certain forms of recursion that are clearly seen to terminate (e.g. decrease const argument by 1 under greater-than-constant test, as in double above), similarly to how we currently allow only certain forms of loops that are clearly seen to terminate.

Another approach is to keep inlining, but fail when a certain limit is reached, or when previously seen const argument values are reached again. (Aside: a similar approach could be also used for general while loops.) I would prefer a more predictable approach, partly because ideally the Leo documentation should explain to users which recursions are allowed and which ones are not.

Borrowing ideas from the termination analysis in theorem provers like ACL2, a recursion should be const-bounded if there is some measure of some subset of the const arguments that decreases according to some well-founded relation in each recursive call, under the tests governing the call. In the double example, the following holds

count > 1 ==> count - 1 < count

but in the forever example the following does not hold

n < n

The requirement applies to every cycle in the call graph, whether it involves a single recursive function or multiple mutually recursive functions.

The proposed restriction that the governing tests do not depend on runtime data seems unnecessary in general. This is a manual inlining of a slight variant of the double example that involves the test sum < 30:

function double(const count: u32, sum: u32) -> u32 {
    if count > 1 && sum < 30 {
        return double(count - 1, sum + sum)
    } else {
        return sum + sum;
    }
}

function main(x: u32) -> u32 {
    return double(3, x)
}

===> {inline call double(3, x)}

function main(x: u32) -> u32 {
    let sum1 = x;
    if 3 > 1 && sum1 < 30 {
        return double(2, sum1 + sum1)
    } else {
        return sum1 + sum1;
    }
}

===> {simplify}

function main(x: u32) -> u32 {
    let sum1 = x;
    if sum1 < 30 {
        return double(2, sum1 + sum1)
    } else {
        return sum1 + sum1;
    }
}

===> {inline call double(2, sum1 + sum1)}

function main(x: u32) -> u32 {
    let sum1 = x;
    if sum1 < 30 {
        let sum2 = sum1 + sum1;
        if 2 > 1 && sum2 < 30 {
            return double(1, sum2 + sum2)
        } else {
            return sum2 + sum2;
        }
    } else {
        return sum1 + sum1;
    }
}

===> {simplify}

function main(x: u32) -> u32 {
    let sum1 = x;
    if sum1 < 30 {
        let sum2 = sum1 + sum1;
        if sum2 < 30 {
            return double(1, sum2 + sum2)
        } else {
            return sum2 + sum2;
        }
    } else {
        return sum1 + sum1;
    }
}

===> {inline call double(1, sum2 + sum2)}

function main(x: u32) -> u32 {
    let sum1 = x;
    if sum1 < 30 {
        let sum2 = sum1 + sum1;
        if sum2 < 30 {
            let sum3 = sum2 + sum2;
            if 1 > 1 && sum3 < 30 {
                return double(0, sum3 + sum3)
            } else {
                return sum3 + sum3;
            }
        } else {
            return sum2 + sum2;
        }
    } else {
        return sum1 + sum1;
    }
}

===> {simplify}

function main(x: u32) -> u32 {
    let sum1 = x;
    if sum1 < 30 {
        let sum2 = sum1 + sum1;
        if sum2 < 30 {
            let sum3 = sum2 + sum2;
            return sum3 + sum3;
        } else {
            return sum2 + sum2;
        }
    } else {
        return sum1 + sum1;
    }
}

This is a manual inlining of a version without the sum < 30 test:

function double(const count: u32, sum: u32) -> u32 {
    if count > 1 {
        return double(count - 1, sum + sum)
    } else {
        return sum + sum;
    }
}

function main(x: u32) -> u32 {
    return double(3, x)
}

===> {inline call double(3, x)}

function main(x: u32) -> u32 {
    let sum1 = x;
    if 3 > 1 {
        return double(2, sum1 + sum1)
    } else {
        return sum1 + sum1;
    }
}

===> {simplify}

function main(x: u32) -> u32 {
    let sum1 = x;
    return double(2, sum1 + sum1)
}

===> {inine call double(2, sum1 + sum1)}

function main(x: u32) -> u32 {
    let sum1 = x;
    let sum2  = sum1 + sum1;
    if 2 > 1 {
        return double(1, sum2 + sum2)
    } else {
        return sum2 + sum2;
    }
}

===> {simplify}

function main(x: u32) -> u32 {
    let sum1 = x;
    let sum2  = sum1 + sum1;
    return double(1, sum2 + sum2)
}

===> {inline call double(1, sum2 + sum2)}

function main(x: u32) -> u32 {
    let sum1 = x;
    let sum2  = sum1 + sum1;
    let sum3 = sum2 + sum2;
    if 1 > 1 {
        return double(0, sum3 + sum3)
    } else {
        return sum3 + sum3;
    }
}

===> {simplify}

function main(x: u32) -> u32 {
    let sum1 = x;
    let sum2  = sum1 + sum1;
    let sum3 = sum2 + sum2;
    return sum3 + sum3;
}