Lambda the Ultimate

I rejected the Haskell-style lazy evaluation as a default in my language, though it's still accessible via explicit annotations.

Granted, my language is combinator based with explicit copy `c :: s * a -> (s * a) * a`, and potential substructural type annotations (to restrict copy or drop for some values). Between these, there is a significant impact on algorithms design assuming linear data structures or Huet zippers instead of copying on access/map/iteration/etc.. Consequently, there is rarely unnecessary sharing. My default 'sharing' strategy is just to deep eval upon copy, unless annotated otherwise.

A `(lazy)` annotation will mark a value to be copied without evaluation, wrapping it within a single assignment hole for the evaluated result. I find this feature is rather awkward with respect to serialization and incremental computing. It's also a bad for for scenarios like exploring a large, procedurally generated model where storage costs can quickly exceed recomputation overheads; for that, we need something closer to caching.

I find that `(memo)`, to memoize computations via indexing an external table, which is not guaranteed to keep all data indefinitely, is a lot cleaner and easier to control and tune regarding memory overheads vs. recompute overheads. It works easily with serialization and durability. It's very suitable for sharing efforts in context of incremental computing, e.g. we can memoize recursive computations over persistent data structures, make a slight change at O(log(N)) costs, and compute again, reusing computations for most of the structure. It's good for caching partial computations of large models, since old resources can be released. Albeit, it's also more expensive than laziness because indexing computations is non-trivial.

I'd be interested in a performance comparison of default laziness with a strategy of evaluate-on-first-copy, memoization tables, or the conventional eager evaluation. Ideally in context of how algorithms are fitted to the evaluation model.

Hi Charles,

I think the most promising application of work in this space (including related things like atomic lambda calculus) is in the implementation of conversion or judgmental equality in dependent type theory. This is a situation where both

a) simple evaluation strategies such as call-by-name, call-by-value, or weak-head reduction frequently hit pathological cases (where you end up evaluating large computations unnecessarily, or end up recompute the same term too frequently),
b) but at the same time, the absolute performance required is not high, so it's fine to spend a lot of effort on book-keeping to avoid the pathological cases.

Alas, there are only so many hours in the day!

Are you talking about Homotopy Type Theory here? I haven't really looked at how complex equality propositions are to prove and how much sharing they might need: it is a thought-provoking idea.

While optimal reduction is known to be efficient for evaluating ELL- and LLL-typable λ-terms, it is an open question whether there exists an efficient implementation of optimal reduction for arbitrary untyped λ-terms without the so-called oracle (consisted of brackets and croissants in BOHM and scope operators in Lambdascope).

Recently, there has been some effort towards a universal modification of Lamping's abstract algorithm, resulting in a possible solution (arXiv:1710.07516) which is still waiting to be (dis)proved. Any help with finding counterexamples or checking the algorithm's correctness would be highly appreciated.