[fourteenminutes]

Yes - if the closure representation is recursive, it must be boxed. I believe your example is also that given by the original author (William Brandon et.al.). I don’t think there is any way around this, because it is the same as any other recursive data type at that point.

Although, if you know at compile time the size of the list, you could imagine compiling the recursive data type “unrolled” into a statically-sized array - but now you need dependent types.

[anfelor]

Ah thanks! I didn't find that paper, is it online somewhere?

You may also be interested in the stack allocation system in OCaml: https://www.youtube.com/watch?v=yGRn5ZIbEW8 In particular, Stephen gives a nice example in the end how it can avoid some allocations of lambdas (but it also would need to box the closure in the CPS-reverse).

You may also be interested in

  Jeffrey M. Bell, Françoise Bellegarde, and James Hook. “Type-Driven Defunctionalization,” ICFP ’97, . Association for Computing Machinery, New York, NY, USA, 25–37. 1997. doi:10.1145/258948.258953.

and

  Andrew Tolmach, and Dino P Oliva. “From ML to Ada: Strongly-Typed Language Interoperability via Source Translation.” Journal of Functional Programming 8 (4). Cambridge University Press: 367–412. 1998.

who thought about whole-program-defunctionalization before.

[fourteenminutes]

The manuscript is currently unpublished so it’s not available ):

Thanks for the links - I’ve seen them, and it’s interesting that defunctionalization is usually an optimization. The “Type-driven …” paper is the earliest work I’m aware of that does it over surface types, but doesnt “go all the way”.

Id love to chat more - a link to email can be found around the post, including at the bottom.