We revisit the polarized L calculus, an abstract-machine-like calculus with mixed evaluation order (i.e. call-by-name and call-by-value) and pattern-matches, and its relation to the λ-calculus. We then show that it is a more symmetric syntax for call-by-push-value. We also introduce a dynamically typed / bi-typed variant of this calculus which completely eliminates clashes (i.e. pattern-matching failures) without relying on any form of typing judgments, and illustrate its usefulness in the study of extensions of the untyped λ-calculus with constructors.
Timeline: