The code in the termination* branch series implements termination proofs of the λτ language following §9 in Jhala–Vazou. This is strictly necessary before we can have the Agda-style λπ of §10, because otherwise λπ can prove False by circularity.
Unfortunately, in Jhala–Vazou the λτ language is backwards-incompatible with the let rec examples in the preceding chapters. This is fine for the didactic nature of their tutorial; however it is a problem in MachineArithmetic where we use sprite-lang/test/* as part of our test suite, and we only have one "comprehensive" language which we want to accept everything in L₁ through L₈.
In LiquidHaskell, the lazy annotation turns termination checking off, similar to Admitted in Coq. We can modify our let rec grammar along similar lines to allow graceful switching between L₁—L₆ and L₇. I think I would prefer the switch to default to the "lazy" behavior so we don't have to touch the tests that are already in CI. So the L₇ tests would have something like let strict-rec.
The code in the
termination*
branch series implements termination proofs of the λτ language following §9 in Jhala–Vazou. This is strictly necessary before we can have the Agda-style λπ of §10, because otherwise λπ can proveFalse
by circularity.Unfortunately, in Jhala–Vazou the λτ language is backwards-incompatible with the
let rec
examples in the preceding chapters. This is fine for the didactic nature of their tutorial; however it is a problem in MachineArithmetic where we usesprite-lang/test/*
as part of our test suite, and we only have one "comprehensive" language which we want to accept everything in L₁ through L₈.In LiquidHaskell, the
lazy
annotation turns termination checking off, similar toAdmitted
in Coq. We can modify ourlet rec
grammar along similar lines to allow graceful switching between L₁—L₆ and L₇. I think I would prefer the switch to default to the "lazy" behavior so we don't have to touch the tests that are already in CI. So the L₇ tests would have something likelet strict-rec
.