-
Monadic Intersection Types, Relationally (Extended Version)
Authors:
Francesco Gavazzo,
Riccardo Treglia,
Gabriele Vanoni
Abstract:
We extend intersection types to a computational $λ$-calculus with algebraic operations à la Plotkin and Power. We achieve this by considering monadic intersections, whereby computational effects appear not only in the operational semantics, but also in the type system. Since in the effectful setting termination is not anymore the only property of interest, we want to analyze the interactive behavi…
▽ More
We extend intersection types to a computational $λ$-calculus with algebraic operations à la Plotkin and Power. We achieve this by considering monadic intersections, whereby computational effects appear not only in the operational semantics, but also in the type system. Since in the effectful setting termination is not anymore the only property of interest, we want to analyze the interactive behavior of typed programs with the environment. Indeed, our type system is able to characterize the natural notion of observation, both in the finite and in the infinitary setting, and for a wide class of effects, such as output, cost, pure and probabilistic nondeterminism, and combinations thereof. The main technical tool is a novel combination of syntactic techniques with abstract relational reasoning, which allows us to lift all the required notions, e.g. of typability and logical relation, to the monadic setting.
△ Less
Submitted 23 January, 2024;
originally announced January 2024.
-
From Semantics to Types: the Case of the Imperative lambda-Calculus
Authors:
Ugo de'Liguoro,
Riccardo Treglia
Abstract:
We propose an intersection type system for an imperative lambda-calculus based on a state monad and equipped with algebraic operations to read and write to the store. The system is 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 lambda-calculus. Then the type sys…
▽ More
We propose an intersection type system for an imperative lambda-calculus based on a state monad and equipped with algebraic operations to read and write to the store. The system is 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 lambda-calculus. 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, and it is sound and complete by construction.
△ Less
Submitted 28 December, 2021;
originally announced December 2021.
-
On reduction and normalization in the computational core
Authors:
Claudia Faggian,
Giulio Guerrieri,
Ugo de'Liguoro,
Riccardo Treglia
Abstract:
We study the reduction in a lambda-calculus derived from Moggi's computational one, that we call the computational core. The reduction relation consists of rules obtained by orienting three monadic laws. Such laws, in particular associativity and identity, introduce intricacies in the operational analysis. We investigate the central notions of returning a value versus having a normal form, and add…
▽ More
We study the reduction in a lambda-calculus derived from Moggi's computational one, that we call the computational core. The reduction relation consists of rules obtained by orienting three monadic laws. Such laws, in particular associativity and identity, introduce intricacies in the operational analysis. We investigate the central notions of returning a value versus having a normal form, and address the question of normalizing strategies. Our analysis relies on factorization results.
△ Less
Submitted 29 November, 2022; v1 submitted 20 April, 2021;
originally announced April 2021.
-
Intersection Types for a Computational Lambda-Calculus with Global State
Authors:
Ugo de'Liguoro,
Riccardo Treglia
Abstract:
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 operational and denotational semantics and a type assignment system of intersection types and prove that types are invariant und…
▽ More
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 operational and denotational semantics and a type assignment system of intersection types and prove that types are invariant under the reduction and expansion of term and state configurations. Finally, we characterize convergent terms via their ty**s.
△ Less
Submitted 4 September, 2022; v1 submitted 3 April, 2021;
originally announced April 2021.
-
Intersection Types for the Computational lambda-Calculus
Authors:
Ugo de'Liguoro,
Riccardo Treglia
Abstract:
We study polymorphic type assignment systems for untyped lambda-calculi with effects, based on Moggi's monadic approach. Moving from the abstract definition of monads, we introduce a version of the call-by-value computational lambda-calculus based on Wadler's variant with unit and bind combinators, and without let. We define a notion of reduction for the calculus and prove it confluent, and also w…
▽ More
We study polymorphic type assignment systems for untyped lambda-calculi with effects, based on Moggi's monadic approach. Moving from the abstract definition of monads, we introduce a version of the call-by-value computational lambda-calculus based on Wadler's variant with unit and bind combinators, and without let. We define a notion of reduction for the calculus and prove it confluent, and also we relate our calculus to the original work by Moggi showing that his untyped metalanguage can be interpreted and simulated in our calculus. We then introduce an intersection type system inspired to Barendregt, Coppo and Dezani system for ordinary untyped lambda-calculus, establishing type invariance under conversion, and provide models of the calculus via inverse limit and filter model constructions and relate them. We prove soundness and completeness of the type system, together with subject reduction and expansion properties. Finally, we introduce a notion of convergence, which is precisely related to reduction, and characterize convergent terms via their types.
△ Less
Submitted 7 February, 2020; v1 submitted 12 July, 2019;
originally announced July 2019.
