Quantitative Types for the Functional Machine Calculus

TL;DR

This paper introduces a quantitative type system for the Functional Machine Calculus (FMC), linking typeability with termination and evaluation metrics, and extending to effects like mutable store, I/O, and probabilistic choice.

Contribution

It develops a discipline of non-idempotent intersection types for FMC, providing precise measures of evaluation and termination properties, including effects.

Findings

Typeability coincides with termination and normalization.

Quantitative types measure evaluation steps and bounds.

Typeability characterizes termination for effects like mutable store, I/O, and probabilistic choice.

Abstract

The Functional Machine Calculus (FMC, Heijltjes 2022) extends the lambda-calculus with the computational effects of global mutable store, input/output, and probabilistic choice while maintaining confluent reduction and simply-typed strong normalization. Based in a simple call-by-name stack machine in the style of Krivine, the FMC models effects through additional argument stacks, and introduces sequential composition through a continuation stack to encode call-by-value behaviour, where simple types guarantee termination of the machine. The present paper provides a discipline of quantitative types, also known as non-idempotent intersection types, for the FMC, in two variants. In the weak variant, typeability coincides with termination of the stack machine and with spine normalization, while exactly measuring the transitions in machine evaluation. The strong variant characterizes strong normalization through a notion of perpetual evaluation, while giving an upper bound to the length of reductions. Through the encoding of effects, quantitative typeability coincides with termination for higher-order mutable store, input/output, and probabilistic choice.