The computational core: reduction theory and intersection type discipline

Moving from the abstract definition of monads, we introduce a version of the call-by-value computational λ-calculus based on Wadler’s variant, without let, and with unit and bind operators. We call the calculus computational core and study its reduction, and prove it confluent. In particular, the reduction rules are the relation obtained by orienting the monadic laws from left to right. The rules induced by associativity and identity make the behaviour of the reduction, and the study of its operational properties, non- trivial. This happens in the setting of any monadic lambda-calculus, independently of the syntactic representation of the calculus that internalizes them. Hence, the focus of our operational analysis is on two crucial properties: returning a value and having a normal form. The cornerstone of our analysis is factorization results. Weak factorization can be achieved by considering the surface reduction relation, a contextual closure of calculi based on linear logic. We expose the operational role of the rules associated with the monadic laws of identity and associativity. We then analyze the property of having a normal form (normalization), and then a family of normalizing strategies, i.e. sub-reductions that are guaranteed to reach a normal form, if any exists. To deal with that we rely on a quantitative analysis of the number of βc-steps. In a second part, we study a Curry style type assignment system for the computational core. We introduce an intersection type system inspired by Barendregt, Coppo, and Dezani system for ordinary untyped λ-calculus, establishing type invariance under conversion. Finally, we introduce a notion of convergence, which is precisely related to reduction, and characterize convergent terms via their types. In the last part, we study the semantics of an untyped lambda-calculus equipped with operators representing read and write operations from and to a global store. We adopt the monadic approach to model side-effects and treat read and write as algebraic operations over a monad. We introduce an operational semantics. The intersection type assignment system is indeed derived by solving a suitable domain equation in the category of omega-algebraic lattices; the solution consists of a filter-model generalizing the well known construction for ordinary lambdacalculus. Then the type system is obtained out of the term interpretations into the filter-model itself. The so obtained type system satisfies the “type-semantics” property (the semantics of a term is precisely the set of types that can be assigned to it) by construction. Finally, we prove that types are invariant under reduction and expansion of term and state configurations, and characterize convergent terms via their typings.