Substructural Simple Type Theories for Separation and In-place Update

Abstract

This thesis studies two substructural simple type theories, extending the "separation" and "number-of-uses" readings of the basic substructural simply typed lambda-calculus with exchange.

The first calculus, lambda_sep, extends the alpha lambda-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, lambda_inplc, is a re-presentation 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 lambda_inplc. To obtain a complete class of models for lambda_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.