The Safety of Call Arity

Abstract

We formalize the Call Arity analysis [Bre15a], as implemented in GHC, and prove both functional correctness and, more interestingly, safety (i.e. the transformation does not increase allocation). A highlevel overview of the work can be found in [Bre15b]. We use syntax and the denotational semantics from an earlier work [Bre13], where we formalized Launchbury’s natural semantics for lazy evaluation [Lau93]. The functional correctness of Call Arity is proved with regard to that deno-tational semantics. The operational properties are shown with regard to a small-step semantics akin to Sestoft’s mark 1 machine [Ses97], which we prove to be equivalent to Launchbury’s semantics. We use Christian Urban’s Nominal2 package [UK12] to define our terms and make use of Brian Huffman’s HOLCF package for the domain-theoretical aspects of the development [Huf12]. Artifact correspondence table The following table connects the definitions and theorems from [Bre15b] with their cor-responding Isabelle concept in this development. Concept corresponds to in theory Syntax nominal-datatype expr Terms in [Bre13] Stack type-synonym stack SestoftConf