research-article

Functors are Type Refinement Systems

Authors:

Paul-André Melliès,

Noam ZeilbergerAuthors Info & Claims

ACM SIGPLAN Notices, Volume 50, Issue 1

Pages 3 - 16

https://doi.org/10.1145/2775051.2676970

Published: 14 January 2015 Publication History

Abstract

The standard reading of type theory through the lens of category theory is based on the idea of viewing a type system as a category of well-typed terms. We propose a basic revision of this reading: rather than interpreting type systems as categories, we describe them as functors from a category of typing derivations to a category of underlying terms. Then, turning this around, we explain how in fact any functor gives rise to a generalized type system, with an abstract notion of typing judgment, typing derivations and typing rules. This leads to a purely categorical reformulation of various natural classes of type systems as natural classes of functors.

The main purpose of this paper is to describe the general framework (which can also be seen as providing a categorical analysis of refinement types), and to present a few applications. As a larger case study, we revisit Reynolds' paper on ``The Meaning of Types'' (2000), showing how the paper's main results may be reconstructed along these lines.

Supplementary Material

MOV File (2676970.mov)

Download
18507.25 MB

References

[1]

Robert Atkey, Patricia Johann, and Neil Ghani. Refining Inductive Types. LMCS, 8:2, 2012.

[2]

Jean Bénabou. Distributors at work.Notes from a course at TU Darmstadt in June 2000, taken by Thomas Streicher.

[3]

Bodil Biering, Lars Birkedal, and Noah Torp-Smith. BI-Hyperdoctrines, Higher-order Separation Logic, and Abstraction. ACM Trans. Program. Lang. Syst., 5:29, 2007.

Digital Library

[4]

Lars Birkedal, Noah Torp-Smith, and Hongseok Yang.Semantics of Separation-Logic Typing and Higher-order Frame Rules for Algol-like languages. LMCS, 5:2, 2006.

[5]

Jacques Carette, Oleg Kiselyov, and Chung-chieh Shan. Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages. JFP, 5:19, 2009.

Digital Library

[6]

Pierre-Evariste Dagand and Conor McBride. A Categorical Treatment of Ornaments. LICS 2013.

Digital Library

[7]

Philippe de Groote. Towards Abstract Categorial Grammars. In Assoc. for Computational Linguistics, 39th Annual Meeting, 2001.

Digital Library

[8]

Andrzej Filinski. Monads in Action. POPL 2010.

Digital Library

[9]

Tim Freeman and Frank Pfenning. Refinement Types for ML. PLDI 1991.

Digital Library

[10]

Robert Harper, Furio Honsell and Gordon Plotkin. A Framework For Defining Logics. Journal of the ACM, 40(1):143--184, 1993.

Digital Library

[11]

Claudio Hermida. Fibrations, Logical predicates and indeterminates, PhD thesis, University of Edinburgh, November 1993.

[12]

C.A.R. Hoare. An Axiomatic Basis for Computer Programming, Communications of the ACM, 12:10, 1969.

Digital Library

[13]

Bart Jacobs. Categorical Logic and Type Theory. Studies in Logic and the Foundations of Mathematics 141. North Holland, 1999.

[14]

Shin-ya Katsumata. Relating Computational Effects by $\top\top$-Lifting. ICALP 2011.

Digital Library

[15]

Max Kelly. Basic concepts in enriched category theory. CUP, 1982.

[16]

Joachim Lambek. The mathematics of sentence structure. American Mathematical Monthly, 65:3, 1958.

[17]

Joachim Lambek and Philip Scott. Introduction to Higher-order Categorical Logic. CUP, 1986.

Digital Library

[18]

F. William Lawvere. Functorial Semantics of Algebraic Theories, PhD thesis, Columbia University, 1963.

[19]

F. William Lawvere. Adjointness in Foundations, Dialectica 23, 1969, 281--296.

[20]

William Lovas. Refinement types for logical frameworks, PhD thesis, Carnegie Mellon University, September 2010.

Digital Library

[21]

Saunders Mac Lane. Categories for the Working Mathematician. Springer, 1971.

[22]

Conor McBride. Ornamental Algebras, Algebraic Ornaments. JFP (to appear). 9/8/2010 version available on author's website.

[23]

Peter W. O'Hearn and David J. Pym. The Logic of Bunched Implications. BSL 5:2, 1999.

[24]

Peter W. O'Hearn and Hongseok Yang. A Semantic Basis for Local Reasoning. FOSSACS 2002.

Digital Library

[25]

Frank J. Oles. A Category-Theoretic Approach to the Semantics of Programming Languages, PhD thesis, Syracuse University, 1982.

Digital Library

[26]

Frank Pfenning. Refinement Types for Logical Frameworks. Workshop on Types for Proofs and Programs, May 1993.

[27]

Frank Pfenning. Church and Curry: Combining Intrinsic and Extrinsic Typing.Studies in Logic 17, 2008, 303--338.

[28]

John C. Reynolds. The Essence of Algol. Algorithmic Languages, 1981, 345--372.

[29]

John C. Reynolds. The Coherence of Languages with Intersection Types, TACS 1991.

Digital Library

[30]

John C. Reynolds. Theories of Programming Languages. CUP, 1998.

Digital Library

[31]

John C. Reynolds. The Meaning of Types: from Intrinsic to Extrinsic Semantics. BRICS Report RS-00--32, Aarhus University, December 2000.

[32]

John C. Reynolds. Separation logic: A Logic for Shared Mutable Data Structures. LICS 2002.

Digital Library

Cited By

Williams CStay M(2022)Native Type TheoryElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.372.9372(116-132)Online publication date: 3-Nov-2022
https://doi.org/10.4204/EPTCS.372.9
Sterling JHarper R(2021)Logical Relations as Types: Proof-Relevant Parametricity for Program ModulesJournal of the ACM10.1145/347483468:6(1-47)Online publication date: 5-Oct-2021
https://dl.acm.org/doi/10.1145/3474834
Olimpieri FGorla D(2021)Intersection type distributorsProceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science10.1109/LICS52264.2021.9470617(1-15)Online publication date: 29-Jun-2021
https://dl.acm.org/doi/10.1109/LICS52264.2021.9470617
Show More Cited By

Index Terms

Functors are Type Refinement Systems
1. Theory of computation
  1. Semantics and reasoning
    1. Program semantics

Recommendations

Functors are Type Refinement Systems
POPL '15: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

The standard reading of type theory through the lens of category theory is based on the idea of viewing a type system as a category of well-typed terms. We propose a basic revision of this reading: rather than interpreting type systems as categories, we ...
The fire triangle: how to mix substitution, dependent elimination, and effects

There is a critical tension between substitution, dependent elimination and effects in type theory. In this paper, we crystallize this tension in the form of a no-go theorem that constitutes the fire triangle of type theory. To release this tension, we ...
Theorems for free!
FPCA '89: Proceedings of the fourth international conference on Functional programming languages and computer architecture

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 50, Issue 1

POPL '15

January 2015

682 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/2775051

Editor:
Andy Gill
University of Kansas, Lawrence, KS

Issue’s Table of Contents

POPL '15: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
January 2015
716 pages
ISBN:9781450333009
DOI:10.1145/2676726
General Chair:
Sriram Rajamani
Microsoft Research, India
,
Program Chair:
David Walker
Princeton University, USA

Copyright © 2015 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 14 January 2015

Published in SIGPLAN Volume 50, Issue 1

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

25
Total Citations
View Citations
732
Total Downloads

Downloads (Last 12 months)41
Downloads (Last 6 weeks)9

Reflects downloads up to 13 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Williams CStay M(2022)Native Type TheoryElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.372.9372(116-132)Online publication date: 3-Nov-2022
https://doi.org/10.4204/EPTCS.372.9
Sterling JHarper R(2021)Logical Relations as Types: Proof-Relevant Parametricity for Program ModulesJournal of the ACM10.1145/347483468:6(1-47)Online publication date: 5-Oct-2021
https://dl.acm.org/doi/10.1145/3474834
Olimpieri FGorla D(2021)Intersection type distributorsProceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science10.1109/LICS52264.2021.9470617(1-15)Online publication date: 29-Jun-2021
https://dl.acm.org/doi/10.1109/LICS52264.2021.9470617
de Amorim AGaboardi MHsu JKatsumata SBouyer P(2019)Probabilistic relational reasoning via metricsProceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science10.5555/3470152.3470192(1-19)Online publication date: 24-Jun-2019
https://dl.acm.org/doi/10.5555/3470152.3470192
Jacq CMelliès P(2018)Categorical Combinatorics for Non Deterministic Strategies on Simple GamesFoundations of Software Science and Computation Structures10.1007/978-3-319-89366-2_3(39-70)Online publication date: 14-Apr-2018
https://doi.org/10.1007/978-3-319-89366-2_3
Oliveira Vale AWang ZChen YYou PShao Z(2024)Compositionality and Observational Refinement for Linearizability with CrashesProceedings of the ACM on Programming Languages10.1145/36897928:OOPSLA2(2296-2324)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689792
van der Weide NRasekh NAhrens BNorth PTimany ATraytel DPientka BBlazy S(2024)Univalent Double CategoriesProceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3636501.3636955(246-259)Online publication date: 9-Jan-2024
https://dl.acm.org/doi/10.1145/3636501.3636955
Economou DKrishnaswami NDunfield J(2023)Focusing on Refinement TypingACM Transactions on Programming Languages and Systems10.1145/361040845:4(1-62)Online publication date: 20-Dec-2023
https://dl.acm.org/doi/10.1145/3610408
Ghalayini JKrishnaswami N(2023)Explicit Refinement TypesProceedings of the ACM on Programming Languages10.1145/36078377:ICFP(187-214)Online publication date: 31-Aug-2023
https://dl.acm.org/doi/10.1145/3607837
Hunt SSands DStucki S(2023)Reconciling Shannon and Scott with a Lattice of Computable InformationProceedings of the ACM on Programming Languages10.1145/35717407:POPL(1987-2016)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571740
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Issue’s Table of Contents