Polarized subtyping

DOI10.1007/978-3-030-99336-8_16zbMATH Open1528.68082arXiv2201.10998OpenAlexW4226343274MaRDI QIDQ6166799FDOQ6166799

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)

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.

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

Recommendations

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

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)

Cites Work

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

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)