Parametricity For Primitive Nested Types
- ASU Author/Contributor (non-ASU co-authors, if there are any, appear on document)
- Patricia Johann Ph.D, Professor (Creator)
- Institution
- Appalachian State University (ASU )
- Web Site: https://library.appstate.edu/
Abstract: This paper considers parametricity and its resulting free theorems for nested data types. Rather than representing nested types via their Church encodings in a higher-kinded or dependently typed extension of System F, we adopt a functional programming perspective and design a Hindley-Milner-style calculus with primitives for constructing nested types directly as fixpoints. Our calculus can express all nested types appearing in the literature, including truly nested types. At the term level, it supports primitive pattern matching, map functions, and fold combinators for nested types. Our main contribution is the construction of a parametric model for our calculus. This is both delicate and challenging: to ensure the existence of semantic fixpoints interpreting nested types, and thus to establish a suitable Identity Extension Lemma for our calculus, our type system must explicitly track functoriality of types, and co-continuity conditions on the functors interpreting them must be appropriately threaded throughout the model construction. We prove that our model satisfies an appropriate Abstraction Theorem and verifies all standard consequences of parametricity for primitive nested types.
Parametricity For Primitive Nested Types
PDF (Portable Document Format)
373 KB
Created on 9/15/2021
Views: 620
Additional Information
- Publication
- Johann, P., Ghiorzi, E., & Jeffries, D. (2021). Parametricity for Primitive Nested Types. Proceedings, Foundations of Software Science and Computation Structures 2021, pp. 324-343. This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. NC Docks permission to re-print granted by author(s).
- Language: English
- Date: 2021
- Keywords
- parametricity, nested data types, Church encodings, fixpoints, Abstraction Theorem, Identity Extension Lemma, parametric model