Substructural Simple Type Theories for Separation and In-place Update
Publication Information
Abstract
This thesis studies two substructural simple type theories, extending the "separation" and "number-of-uses" readings of the basic substructural simply typed λ-calculus with exchange.
The first calculus, λsep, extends the αλ-calculus of O'Hearn and Pym by directly considering the representation of separation in a type system. We define type contexts with separation relations and introduce new type constructors of separated products and separated functions. We describe the basic metatheory of the calculus, including a sound and complete type-checking algorithm. We then give new categorical structure for interpreting the type judgements, and prove that it coherently, soundly and completely interprets the type theory. To show how the structure models separation we extend Day's construction of closed symmetric monoidal structure on functor categories to our categorical structure, and describe two instances dealing with the global and local separation.
The second system, λinplc, is a re-presentation a of substructural calculus for in-place update with linear and non-linear values, based on Wadler's Linear typed system with non-linear types and Hofmann's LFPL. We identify some problems with the metatheory of the calculus, in particular the failure of the substitution rule to hold due to the call-by-value interpretation inherent in the type rules. To resolve this issue, we turn to categorical models of call-by-value computation, namely Moggi's Computational Monads and Power and Robinson's Freyd-Categories. We extend both of these to include additional information about the current state of the computation, defining Parameterised Freyd-categories and Parameterised Strong Monads. These definitions are equivalent in the closed case. We prove that by adding a commutativity condition they are a sound class of models for λinplc. To obtain a complete class of models for λinplc we refine the structure to better match the syntax. We also give a direct syntactic presentation of Parameterised Freyd-categories and prove that it is soundly and completely modelled by the syntax. We give a concrete model based on Day's construction, demonstrating how the categorical structure can be used to model call-by-value computation with in-place update and bounded heaps.
Additional Information
This thesis was supervised by David Aspinall, with Ian Stark my second supervisor. John Longley and Alex Simpson also participated in the panel meetings.
The first part of this thesis, on an extension of the αλ-calculus, was published in an ICALP 2004 conference paper. The second half, on parameterised monads was first published as a workshop paper at MSFP 2006 and then revised and expanded for a paper in the Journal of Functional Programming.