When Programs Have to Watch Paint Dry

TL;DR

This paper introduces a novel type system and programming abstractions for managing temporal resources, ensuring safe and modular handling of time-dependent operations like drying paint in automated processes.

Contribution

It develops a time-graded Fitch-style modal type system, a corresponding effect calculus with temporally-aware algebraic effects, and a presheaf model to reason about time-sensitive resource usage.

Findings

A new temporal treatment for graded algebraic effects.

A modal type system for specifying resource timing constraints.

A denotational semantics model illustrating the approach.

Abstract

We explore type systems and programming abstractions for the safe use of resources. In particular, we investigate how to use types to modularly specify and check when programs are allowed to use their resources, e.g., when programming a robot arm on a production line, it is crucial that painted parts are given enough time to dry before assembly. We capture such temporal resources using a time-graded variant of Fitch-style modal type systems, develop a corresponding modally typed, effectful core calculus, and equip it with a graded-monadic denotational semantics illustrated by a concrete presheaf model. Our calculus also includes temporally-aware graded algebraic effects and effect handlers. The former are given a novel temporal treatment, where operations' specifications include their execution times, and their continuations know that an operation's worth of additional time has passed before they start executing, making it possible to safely access further temporal resources in them, and where effect handlers have to respect this temporal discipline.