The structure of call-by-value
MetadataShow full item record
Understanding procedure calls is crucial in computer science and everyday programming. Among the most common strategies for passing procedure arguments ('evaluation strategies') are 'call-by-name', 'call-by-need', and 'call-by-value', where the latter is the most commonly used. While reasoning about procedure calls is simple for call-by-name, problems arise for call-by-need and call-by-value, because it matters how often and in which order the arguments of a procedure are evaluated. We shall classify these problems and see that all of them occur for call-by-value, some occur for call-by-need, and none occur for call-by-name. In that sense, call-by-value is the 'greatest common denominator' of the three evaluation strategies. Reasoning about call-by-value programs has been tackled by Eugenio Moggi's 'computational lambda-calculus', which is based on a distinction between 'values' and arbitrary expressions. However, the computational lambda-calculus deals only implicitly with the evaluation order and the number of evaluations of procedure arguments. Therefore, certain program equivalences that we should be able to spot immediately require long proofs. We shall remedy this by introducing a new calculus - the 'let-calculus' - that deals explicitly with evaluation order and the number of evaluations. For dealing with the number of evaluations, the let-calculus has mechanisms known from; linear, affine, and relevant logic. For dealing with evaluation order, it has mechanisms which seems to be completely new. We shall also introduce a new kind of denotational semantics for call-by-value programming languages. The key idea is to consider how categories with finite products are commonly used to model call-by-name languages, and remove the axioms which break for call-by-value. The resulting models we shall call 'precartesian categories'. These relatively simple structures have remarkable mathematical properties, which will inspire the design of the let-calculus. Precartesian categories will provide a semantics of both the let-calculus and the computational lambda-calculus. This semantics not only validates the same program equivalences as Moggi's monad-based semantics of the computational lambda-calculus; It is also 'direct' by contrast to Moggi's semantics, which implicitly performs a language transform. Our direct semantics has practical benefits: It clarifies issues that are related with the evaluation order and the number of evaluations of procedure arguments, and it is also very easy to remember. The thesis is rounded up by three applications of the let-calculus and precartesian categories: First, construing well-established models of partiality (i.e. categories of generalised partial functions) as precartesian categories, and specialising the let-calculus accordingly. Second, adding global state to a given computational system and construing the resulting system as a precartesian category. Third, analysing an implementation technique called 'continuation-style transform' by construing the source language of such a transform as a precartesian category.