The Cost of Skeletal Call-by-Need, Smoothly

TL;DR

This paper analyzes the cost of skeletal call-by-need evaluation, showing it can be exponentially faster than traditional call-by-need and can be implemented efficiently with bi-linear overhead.

Contribution

It provides the first exponential speedup examples for skeletal call-by-need and introduces a smooth implementation approach with bi-linear overhead.

Findings

Skeletal call-by-need can be exponentially faster than call-by-need.

Efficient implementation of skeletal call-by-need with bi-linear overhead.

A new smooth presentation for skeleton reconstruction.

Abstract

Skeletal call-by-need is an optimization of call-by-need evaluation also known as "fully lazy sharing": when the duplication of a value has to take place, it is first split into "skeleton", which is then duplicated, and "flesh" which is instead kept shared. Here, we provide two cost analyses of skeletal call-by-need. Firstly, we provide a family of terms showing that skeletal call-by-need can be asymptotically exponentially faster than call-by-need in both time and space; it is the first such evidence, to our knowledge. Secondly, we prove that skeletal call-by-need can be implemented efficiently, that is, with bi-linear overhead. This result is obtained by providing a new smooth presentation of ideas by Shivers and Wand for the reconstruction of skeletons, which is then smoothly plugged into the study of an abstract machine following the distillation technique by Accattoli et al.