Stack trace for blame failures

[teofr]

The basic idea of this stack trace is to provide a dynamic path of an execution leading to a Blame . This should be easily extended to other kinds of errors.

On a higher order language it's not straight forward what does it mean to call a function (or to enter a function), this approach takes as calling (entering) any time the evaluator looks up a var on the environment. But at the same time it differentiates between two different kinds of vars, let-bound or lambda-bound. I think this provides a good level of detail of what's going on.

There are some examples, here's one ( trace.ncl ):

Code:

let map = Assume((Num -> Num) -> Num, fun funky => (funky 3) + (funky false)) in
map (fun yak => yak + 1)

Output:

Evaluation didn't finished, found error:
Reached a blame label, some cast went terribly wrong
    Tag: An assume
    Line: 1 Column: 11

CallStack:
    Bounded to yak on line: 2 col: 17
    Bounded to funky on line: 1 col: 65
On a call to map on line: 2 col: 1

The basic idea is that we now can know:

• Which contract failed (with First experiments on improving the label #23 we could know which part of the contract)
• And also which call to funky, which is an anonymous lambda

Ideally, we could combine #23 and this information (the stack also has information for every application) in order to say which part violated which subcontract of the failing contract

[teofr]

Rebased.

[aspiwack]

I'm not convinced that the lambda-binder part of the trace is very relevant, to be honest. But it's not hard to remove either.

[teofr]

I think the main use for lambda binders is when you use higher order functions, and specially when you combine these with anonymous functions, for example:

let map = Assume((Num -> Num) -> Num, fun funky => (funky 3) + (funky false)) in
map (fun yak => yak + 1)

Gives the following trace:

CallStack:
=========
    Bounded to yak on line: 2 col: 17
    Bounded to funky on line: 1 col: 65
On a call to map on line: 2 col: 1

Without the lambda-binder part you wouldn't know:

• which call to funky caused a problem,
• the fact that fun yak => yak + 1 was ever executed.