-
Polymorphic Records for Dynamic Languages
Authors:
Giuseppe Castagna,
Loïc Peyrot
Abstract:
We define and study "row polymorphism" for a type system with set-theoretic types, specifically union, intersection, and negation types. We consider record types that embed row variables and define a subty** relation by interpreting types into sets of record values and by defining subty** as the containment of interpretations. We define a functional calculus equipped with operations for field…
▽ More
We define and study "row polymorphism" for a type system with set-theoretic types, specifically union, intersection, and negation types. We consider record types that embed row variables and define a subty** relation by interpreting types into sets of record values and by defining subty** as the containment of interpretations. We define a functional calculus equipped with operations for field extension, selection, and deletion, its operational semantics, and a type system that we prove to be sound. We provide algorithms for deciding the ty** and subty** relations.
This research is motivated by the current trend of defining static type system for dynamic languages and, in our case, by an ongoing effort of endowing the Elixir programming language with a gradual type system.
△ Less
Submitted 30 March, 2024;
originally announced April 2024.
-
Node Replication: Theory And Practice
Authors:
Delia Kesner,
Loïc Peyrot,
Daniel Ventura
Abstract:
We define and study a term calculus implementing higher-order node replication. It is used to specify two different (weak) evaluation strategies: call-by-name and fully lazy call-by-need, that are shown to be observationally equivalent by using type theoretical technical tools.
We define and study a term calculus implementing higher-order node replication. It is used to specify two different (weak) evaluation strategies: call-by-name and fully lazy call-by-need, that are shown to be observationally equivalent by using type theoretical technical tools.
△ Less
Submitted 19 January, 2024; v1 submitted 14 July, 2022;
originally announced July 2022.
-
A Faithful and Quantitative Notion of Distant Reduction for the Lambda-Calculus with Generalized Applications
Authors:
José Espírito Santo,
Delia Kesner,
Loïc Peyrot
Abstract:
We introduce a call-by-name lambda-calculus $λJn$ with generalized applications which is equipped with distant reduction. This allows to unblock $β$-redexes without resorting to the standard permutative conversions of generalized applications used in the original $ΛJ$-calculus with generalized applications of Joachimski and Matthes. We show strong normalization of simply-typed terms, and we then f…
▽ More
We introduce a call-by-name lambda-calculus $λJn$ with generalized applications which is equipped with distant reduction. This allows to unblock $β$-redexes without resorting to the standard permutative conversions of generalized applications used in the original $ΛJ$-calculus with generalized applications of Joachimski and Matthes. We show strong normalization of simply-typed terms, and we then fully characterize strong normalization by means of a quantitative (i.e. non-idempotent intersection) ty** system. This characterization uses a non-trivial inductive definition of strong normalization --related to others in the literature--, which is based on a weak-head normalizing strategy. We also show that our calculus $λJn$ relates to explicit substitution calculi by means of a faithful translation, in the sense that it preserves strong normalization. Moreover, our calculus $λJn$ and the original $ΛJ$-calculus determine equivalent notions of strong normalization. As a consequence, $λJ$ inherits a faithful translation into explicit substitutions, and its strong normalization can also be characterized by the quantitative ty** system designed for $λJn$, despite the fact that quantitative subject reduction fails for permutative conversions.
△ Less
Submitted 9 January, 2024; v1 submitted 11 January, 2022;
originally announced January 2022.
