Lambda the Ultimate

Coq developpers recently put together a survey of their tool usage, which will hopefully inform future evolutions. From Matthieu Sozeau's announcement:

On behalf of the Coq developers, I’d like to invite everyone to respond to a survey on their usage of Coq, its programming and proving environment, development model, shortcomings and future directions. This survey aims at gathering important information about Coq's users and uses. The results will be used to better understand users' needs, and help decide in which direction Coq’s development should go. It is really important for us to get as many answers as possible before * January 15th 2014 *. We are also taking this occasion to collaboratively build a bibliography of Coq-related papers. The survey’s results will be synthesized, anonymized and made publicly available in february.

The estimated burden time for this survey is around 30 minutes. The survey is available online at:

https://sondages.inria.fr/index.php/276926/lang-en

This survey was mainly prepared by Thomas Braibant, assisted by Enrico Tassi, thanks to them for giving us all an occasion to take a step back and reflect on Coq’s future.

So I've been working on a new language for a while and the topic of how to implement closures came up. I have seen closures usually implemented on the heap or with some malloc region of memory. This seems suboptimal so I thought of it some more and came up with the idea of using type unions to store local variables. This way closures could be passed around on the stack normally.

Obviously this has downsides if you hold too many local variables or few large ones. Since this has probably been done before, I would like to ask the community what their experiences have been with alternative closure implementations.

Also to note, specialization of functions is an option that could help reign in the size of the closure struct.