revisit cast errors

Question

revisit cast errors

Closed this issue 7 years ago · 3 comments

I closed #14 because the last theorem was false -- some errors do step. For example if d1 steps but d2 is a cast error, d1 (d2) is both an error and steps.

This goes against my (the) intuition that the branches of progress ought to be disjoint as a principle. We should either change casts so that they accumulate through evaluation but stepping happens beyond them or figure out a good reason why it's ok that the branches aren't disjoint.

Answer 1 · 2018-02-06T05:20:56.000Z

the 2/6 version of the notes posted on slack have an initial design for this idea. the new forms/rules/clauses are starred in red for easy diffing. let me know what you think.

Answer 2 · 2018-02-06T05:21:18.000Z

"this idea" being "treat failed casts as indeterminate forms"

Answer 3 · 2018-02-07T20:33:13.000Z

i think we've accepted this proposal, so i'm closing this in favor of #33 , which is actually actionable stuff for me to do in agda.