AI summaryⓘ
The authors use a special math system called the tropical semiring to track how programs use time when running. They create a type system where a number on a function parameter means the value will be available after that many time steps, helping ensure the program keeps producing results without getting stuck. They develop two formal setups: one with recursive and polymorphic types that guarantees productivity, and another that uses a new kind of typing with "timed" sets to precisely describe when terms become available. Their work proves that the terms you can type exactly match productive programs, and that deciding if a term can be typed is as complex as possible within a certain logical classification.
tropical semiringgraded coeffect typingproductivityrecursive typespolymorphic typesNakano's later modalityintersection typinghereditarily head normal formsarithmetical hierarchyΠ0^2 property
Abstract
We show that the tropical semiring over the natural numbers, when used as the grading space in graded coeffect typing, faithfully models the passage of time while simultaneously guaranteeing productivity of well-typed programs. A grade a, when assigned to a function parameter, indicates that the parameter is not necessarily available immediately, but will become available after a time steps. We investigate this idea through two formal systems. We first introduce a graded type system featuring recursive and polymorphic types, and show that, in this setting, a natural restriction on recursive types is sufficient to guarantee productivity, while still allowing the definition of streams and recursive programs on them. In particular, we prove that Nakano's later modality can be embedded directly into our system. We then show that tropical grading naturally suggests a novel form of intersection typing, in which the role traditionally played by sets or multisets of types is instead taken by "timed" sets, i.e., functions assigning to each type A the earliest time, represented as a grade, from which the underlying term is available with type A. For the resulting system, we prove not only that productivity is guaranteed, but that it is also characterized: the typable terms are exactly those with hereditarily head normal forms. Remarkably, the system is recursion-theoretically optimal, i.e., typability can be directly proved to be a $Π_0^2$ property in the arithmetical hierarchy.