Thorin

Thorin is an Intermediate Representation that combines Compiling with Continuations and Sea of Nodes.

fac(n : int, ret : fn(int)):
  branch(fac.n <= 0, then, else)

then():
  ret(1)

else():
  head(2, 1)

head(i : int, r : int):
  branch(head.i <= fac.n, body, next)

body():
  head(head.i+1, head.i*head.r)

next():
  fac.ret(head.r)

Unlike CPS representations, Thorin implements continuation nesting implicitly. This lets us avoid let floating/sinking passes when doing optimization passes. We accomplish this by allowing continuations to refer to other continuations parameters, thus establishing an implicit nesting via a data dependency edge.

main: fac(2, k)

Andras Kovacs said this:

So I looked at the paper and your nbe and I have to say I'm not convinced by Thorin. I don't see how to maintain a global CSE store, which is very useful for, well, CSE, but also important for eta-reductions, because I want to test in constant time if a value is of the form (fst x, snd x) after taking into account all de-duplications. Also for eta-reducing case splits. Nested lexical scoping is good for NbE style optimization passes, because when we do a linear traversal over all code, we have more information about computational contexts at any given program point. The blockless IR seems more suited to massaging it in order to make it better. But I like it more to have IR-s as storage formats at "checkpoints", to be evaluated into semantic domains and then read back. This IR should be relatively compact but should also preserve as much as possible info that's relevant for further optimization.

Not too bad, that's what I would try to do in my own CSE for mutual recursion, but in Thorin I think the more annoying thing is that ordinary non-recursive functions are just also not hash-consable immediately up to alpha

We can add all free vars as formal De Bruijn level args (for instance) to functions, and instantiate them to callsites, and explicitly mark recursive groups, and that would solve this

Quotation

Quotation of Thorin terms is quite difficult; it is unclear exactly how we read back a continuation.

What if we lean more into the CPS transform?

const(a):
  ret(k[a])

k[a](b):
  ret(a)