The `repeat` syntax of gradual typed lambda calculus defined by Racket?

Question

I don't understand what's the meaning of repeat (j l h) in the following code snippet from a paper about gradual typed lambda calculus, the algorithm is quicksort, maybe the syntax definition can be guessed by someone who know the algorithm:

---

Edit: From my current understanding, the algorithm has error, it should be: [i: (Ref Int) (box (- l 1))], i.e. h should be l.

---

link to the paper: https://dl.acm.org/doi/10.1145/3314221.3314627#sec-supp

The source code of their Grift compiler is written in .rkt so I hope if someone know about Racket can help, the repeat syntax is defined here: https://github.com/Gradual-Typing/Grift/blob/95c56d94b38e9b33adf7a662c6d7768430d977da/src/language/syntax.rkt#L126

I'm new to functional programming/Racket/GTLC+, sorry I've tried my best to describe my question...

Answer 1

1. The meaning of repeat(j l h) is for j in a[l]...a[h](inclusive).
2. The meaning of [i: Int (box (- h 1))] initialize a Int variable named i create at heap with value operator-(h, 1).
3. The algorithm has error on the line: [i: (Ref Int) (box (- h 1))], I think it should be [i: (Ref Int) (box (- l 1))], reason: I consider h as high-end and the repeat loop will increment i when condition is met, this may result in i > h which is absurd.