Towards a Direct, By-Need Evaluator for Dependently Typed Languages

TL;DR

This paper introduces a stack machine-based interpreter for the lambda-pi calculus in C, enabling efficient by-need evaluation, syntax recovery, and potential use as a scripting language for scientific workflows.

Contribution

It extends a call-by-need stack machine to handle types and terms uniformly, improving evaluation efficiency and enabling syntax recovery without garbage collection.

Findings

Demonstrates efficient execution of benchmark problems

Shows reduced garbage collection tasks

Provides timing and stack space usage data

Abstract

We present a C-language implementation of the lambda-pi calculus by extending the (call-by-need) stack machine of Ariola, Chang and Felleisen to hold types, using a typeless- tagless- final interpreter strategy. It has the advantage of expressing all operations as folds over terms, including by-need evaluation, recovery of the initial syntax-tree encoding for any term, and eliminating most garbage-collection tasks. These are made possible by a disciplined approach to handling the spine of each term, along with a robust stack-based API. Type inference is not covered in this work, but also derives several advantages from the present stack transformation. Timing and maximum stack space usage results for executing benchmark problems are presented. We discuss how the design choices for this interpreter allow the language to be used as a high-level scripting language for automatic distributed parallel execution of common scientific computing workflows.