Polarized subtyping

DOI10.1007/978-3-030-99336-8_16MaRDI QIDQ6166799zbMATH OpenOpenAlexFDO

Authors Zeeshan Lakhani, Ankush Das, Henry DeYoung, Andreia Mordido, Frank Pfenning

Publication date 3 August 2023

Published in Programming Languages and Systems (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/2201.10998

zbMATH Keywords

subtypingcall-by-push-valuesemantic typing

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70) Functional programming and lambda calculus (68N18)

Abstract: Polarization of types in call-by-push-value naturally leads to the separation of inductively defined observable values (classified by positive types), and coinductively defined computations (classified by negative types), with adjoint modalities mediating between them. Taking this separation as a starting point, we develop a semantic characterization of typing with step indexing to capture observation depth of recursive computations. This semantics justifies a rich set of subtyping rules for an equirecursive variant of call-by-push-value, including variant and lazy records. We further present a bidirectional syntactic typing system for both values and computations that elegantly and pragmatically circumvents difficulties of type inference in the presence of width and depth subtyping for variant and lazy records. We demonstrate the flexibility of our system by systematically deriving related systems of subtyping for (a) isorecursive types, (b) call-by-name, and (c) call-by-value, all using a structural rather than a nominal interpretation of types.

Recommendations

• Polarized Subtyping for Sized Types
• Polarised subtyping for sized types
• On the unity of duality
• Polymorphic lambda calculus and subtyping.
• Positive subtyping

Cites work

• scientific article; zbMATH DE number 1183236 (Why is no real title available?)
• scientific article; zbMATH DE number 3714908 (Why is no real title available?)
• scientific article; zbMATH DE number 42737 (Why is no real title available?)
• scientific article; zbMATH DE number 1956517 (Why is no real title available?)
• scientific article; zbMATH DE number 7561489 (Why is no real title available?)
• A theory of type polymorphism in programming
• Automata, Languages and Programming
• Call-by-push-value: Decomposing call-by-value and call-by-name
• Deforestation, program transformation, and cut-elimination
• Integrating induction and coinduction via closure operators and proof cycles
• Intersection types and computational effects
• Intuitionistic Podelski-Rybalchenko theorem and equivalence between inductive definitions and cyclic proofs
• Linear type theory for asynchronous session types
• Mixed Inductive/Coinductive Types and Strong Normalization
• Nested session types
• On the preciseness of subtyping in session types
• Polarized Subtyping for Sized Types
• Polymorphic functions with set-theoretic types. I: Syntax, semantics, and evaluation
• Polymorphic functions with set-theoretic types. II: Local type inference and type reconstruction
• Positive recursive type assignment
• Practical foundations for programming languages
• Probabilistic call by push value
• Programming Languages and Systems
• Recursive subtyping revealed (functional pearl)
• Resumptions, weak bisimilarity and big-step semantics for While with interactive I/O: an exercise in mixed induction-coinduction
• Semantic subtyping, dealing set-theoretically with function, union, intersection, and negation types
• Sequent calculi for induction and infinite descent
• Set-theoretic types for polymorphic variants
• Structural induction and coinduction in a fibrational setting
• Subtyping for session types in the pi calculus
• Subtyping, declaratively. An exercise in mixed induction and coinduction
• Sums of uncertainty: refinements go gradual
• Tridirectional typechecking
• Type-based termination, inflationary fixed-points, and mixed inductive-coinductive types
• Types and programing languages
• Well-founded recursion with copatterns and sized types
• Wellfounded recursion with copatterns: a unified approach to termination and productivity

Cited in

(4)

• Mixed polarized constructions
• Polarization and isogenies
• Polarized Substructural Session Types
• A strong polarized relation

This page was built for publication: Polarized subtyping

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6166799)