Typed Adapton: Refinement types for incremental computations with precise names

Draft paper arXiv:1610.00097 [cs.PL]

Matthew A. Hammer and Joshua Dunfield and Dimitrios J. Economou and Monal Narasimhamurthy

Abstract

Over the past decade, programming language techniques for incremental computation have demonstrated that incremental programs with precise, carefully chosen dynamic names for data and sub-computations can dramatically outperform non-incremental programs, as well as those using traditional memoization (without such names). However, prior work lacks a verification mechanism to solve the ambiguous name problem, the problem of statically enforcing precise names. We say that an allocated pointer name is precise for an evaluation derivation when it identifies at most one value or subcomputation, and ambiguous otherwise.

In this work, we define a refinement type system that gives practical static approximations to enforce precise, deterministic allocation names in otherwise functional programs. We show that this type system permits expressing familiar functional programs, and generic, composable library components. We prove that our type system enforces that well-typed programs name their values and sub-computations precisely, without ambiguity. Drawing closer to an implementation, we derive a bidirectional version of the type system, and prove that it corresponds to our declarative type system. A key challenge in implementing the bidirectional system is handling constraints over names, name terms and name sets; toward this goal, we give decidable, syntactic rules to guide these checks.

Draft, February 2017

Draft of February 2017 (includes appendix)

BibTeX entry

@Unpublished{Hammer17:types,
  author = {Matthew A. Hammer and Joshua Dunfield and Dimitrios J. Economou and Monal Narasimhamurthy},
  title = {{Typed Adapton}: Refinement types for incremental computations with precise names},
  year = {2017},
  month = feb 
}
  


Joshua Dunfield