Racket 定义的渐进类型 lambda 演算的“重复”语法？

Question

我不明白repeat (j l h)在下面的代码sn-p中是什么意思，来自一篇关于渐进类型lambda演算的论文，算法是快速排序，也许知道算法的人可以猜到语法定义：

---

编辑：根据我目前的理解，算法有错误，应该是：[i: (Ref Int) (box (- l 1))]，即h应该是l。

---

论文链接：https://dl.acm.org/doi/10.1145/3314221.3314627#sec-supp

他们的 Grift 编译器的源代码是用.rkt 编写的，所以我希望如果有人知道 Racket 可以提供帮助，这里定义了重复语法：https://github.com/Gradual-Typing/Grift/blob/95c56d94b38e9b33adf7a662c6d7768430d977da/src/language/syntax.rkt#L126

我是函数式编程/Racket/GTLC+ 的新手，抱歉，我已尽力描述我的问题...

Answer 1

1. repeat(j l h)的含义是for j in a[l]...a[h]（含）。
2. [i: Int (box (- h 1))] 的含义初始化一个名为Int 的变量i 在堆中创建，值为operator-(h, 1)。
3. 算法出错：[i: (Ref Int) (box (- h 1))]，我认为应该是[i: (Ref Int) (box (- l 1))]，原因：我认为h是高端的，当条件满足时repeat循环会增加i , 这可能会导致i > h 这很荒谬。