On Mon, 26 Aug 2013, Michael Norrish wrote:
It's certainly true that I may be wincing unnecessarily about memory. Nonetheless, there will be both a memory *and* time cost with this approach that Haskell, for example, probably wouldn't incur. (I believe Haskell's laziness (and deforestation optimisations?) should in theory ensure that the intermediate data structure doesn't get built or really even traversed. With what we have in SML, we will end up traversing the original term, building something almost isomorphic to that original, and then traversing that copy to actually do the printing. Two traversals, a whole bunch of allocations eventually followed by collections, and then the actual printing. Probably insignificant but it makes me wince.
Maybe. David Matthews could say more about how the Poly/ML runtime system really works, and what matters and what not.
I've myself done a lot of "empirical" performance tuning for Isabelle on Poly/ML in recent years, and the above considerations are rather alien to me now. The real performance happens elsewhere.
Makarius