Speaker:
Michael Arntzenius (Birmingham)
Title:
Type inference for monotonicity
Abstract:
A function is monotone if increasing its input can't decrease its
output. It can be useful to guarantee certain functions in a
program are monotone. For example, iterating a monotone map on a
semilattice satisfying the ascending chain condition will find its
least fixed point; many algorithms are concisely expressed this
way, including shortest paths, NFA equivalence, many static
analyses, and CYK parsing. As another example, recent work in
distributed programming (eg. "Consistency as Logical Monotonicity")
has connected monotonicity with eventual consistency.
I present a work-in-progress bidirectional type inference algorithm
for a simply-typed lambda calculus where types denote preorders and
all functions are monotone. Non-monotonicity is handled with modal
types, but surprisingly, these types need no explicit constructors
or destructors; they can be entirely inferred -- I hope. The crucial
techniques are:
1. annotating variables with their modalities, which form a
semiring;
2. taking advantage of adjunctions in the underlying semantics;
3. being very careful about subtyping.