On the semantic expressiveness of recursive types

Marco Patrignani, Eric Mark Martin, Dominique Devriese

Research output: Contribution to journalArticlepeer-review

4 Citations (Scopus)
68 Downloads (Pure)

Abstract

Recursive types extend the simply-typed lambda calculus (STLC) with the additional expressive power to enable diverging computation and to encode recursive data-types (e.g., lists). Two formulations of recursive types exist: iso-recursive and equi-recursive. The relative advantages of iso-and equi-recursion are well-studied when it comes to their impact on type-inference. However, the relative semantic expressiveness of the two formulations remains unclear so far. This paper studies the semantic expressiveness of STLC with iso-and equi-recursive types, proving that these formulations are equally expressive. In fact, we prove that they are both as expressive as STLC with only term-level recursion. We phrase these equi-expressiveness results in terms of full abstraction of three canonical compilers between these three languages (STLC with iso-, with equi-recursive types and with term-level recursion). Our choice of languages allows us to study expressiveness when interacting over both a simply-typed and a recursively-typed interface. The three proofs all rely on a typed version of a proof technique called approximate backtranslation. Together, our results show that there is no difference in semantic expressiveness between STLCs with iso-and equi-recursive types. In this paper, we focus on a simply-typed setting but we believe our results scale to more powerful type systems like System F.

Original languageEnglish
Article number21
Pages (from-to)1-29
Number of pages29
JournalProceedings of the ACM on Programming Languages
Volume5
Issue numberPOPL
DOIs
Publication statusPublished - 4 Jan 2021
EventPrinciples of Programming Languages -
Duration: 17 Jan 202122 Jan 2021

Bibliographical note

Funding Information:
The authors thank the anonymous reviewers for detailed feedback on an earlier draft as well as Phil Wadler for interesting comments and suggestions. This work was partially supported: by the Office of Naval Research for support through grant N00014-18-1-2620, Accountable Protocol Customization, by the German Federal Ministry of Education and Research (BMBF) through funding for the CISPA-Stanford Center for Cybersecurity (FKZ: 13N1S0762), by the Air Force Office of Scientific Research under award number FA9550-21-1-0054, and by the Fund for Scientific Research -Flanders (FWO).

Funding Information:
This work was partially supported: by the Ofce of Naval Research for support through grant N00014-18-1-2620, Accountable Protocol Customization, by the German Federal Ministry of Education and Research (BMBF) through funding for the CISPA-Stanford Center for Cybersecurity (FKZ: 13N1S0762), by the Air Force Ofce of Scientifc Research under award number FA9550-21-1-0054, and by the Fund for Scientifc Research-Flanders (FWO).

Publisher Copyright:
© 2021 Owner/Author.

Copyright:
Copyright 2021 Elsevier B.V., All rights reserved.

Fingerprint

Dive into the research topics of 'On the semantic expressiveness of recursive types'. Together they form a unique fingerprint.

Cite this