Parametricity for Nested Types and GADTs
This paper considers parametricity and its consequent 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 c...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2021-12-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/7086/pdf |
| _version_ | 1797268504591728640 |
|---|---|
| author | Patricia Johann Enrico Ghiorzi |
| author_facet | Patricia Johann Enrico Ghiorzi |
| author_sort | Patricia Johann |
| collection | DOAJ |
| description | This paper considers parametricity and its consequent 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 level of terms, 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. In particular, 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 cocontinuity conditions on the
functors interpreting them must be appropriately threaded throughout the model
construction. We also prove that our model satisfies an appropriate Abstraction
Theorem, as well as that it verifies all standard consequences of parametricity
in the presence of primitive nested types. We give several concrete examples
illustrating how our model can be used to derive useful free theorems,
including a short cut fusion transformation, for programs over nested types.
Finally, we consider generalizing our results to GADTs, and argue that no
extension of our parametric model for nested types can give a functorial
interpretation of GADTs in terms of left Kan extensions and still be
parametric. |
| first_indexed | 2024-04-25T01:33:32Z |
| format | Article |
| id | doaj.art-8c87a451918f40cbb3213a77098d2ad3 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:33:32Z |
| publishDate | 2021-12-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-8c87a451918f40cbb3213a77098d2ad32024-03-08T10:35:55ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742021-12-01Volume 17, Issue 410.46298/lmcs-17(4:23)20217086Parametricity for Nested Types and GADTsPatricia JohannEnrico Ghiorzihttps://orcid.org/0000-0001-5983-6230This paper considers parametricity and its consequent 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 level of terms, 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. In particular, 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 cocontinuity conditions on the functors interpreting them must be appropriately threaded throughout the model construction. We also prove that our model satisfies an appropriate Abstraction Theorem, as well as that it verifies all standard consequences of parametricity in the presence of primitive nested types. We give several concrete examples illustrating how our model can be used to derive useful free theorems, including a short cut fusion transformation, for programs over nested types. Finally, we consider generalizing our results to GADTs, and argue that no extension of our parametric model for nested types can give a functorial interpretation of GADTs in terms of left Kan extensions and still be parametric.https://lmcs.episciences.org/7086/pdfcomputer science - logic in computer science |
| spellingShingle | Patricia Johann Enrico Ghiorzi Parametricity for Nested Types and GADTs Logical Methods in Computer Science computer science - logic in computer science |
| title | Parametricity for Nested Types and GADTs |
| title_full | Parametricity for Nested Types and GADTs |
| title_fullStr | Parametricity for Nested Types and GADTs |
| title_full_unstemmed | Parametricity for Nested Types and GADTs |
| title_short | Parametricity for Nested Types and GADTs |
| title_sort | parametricity for nested types and gadts |
| topic | computer science - logic in computer science |
| url | https://lmcs.episciences.org/7086/pdf |
| work_keys_str_mv | AT patriciajohann parametricityfornestedtypesandgadts AT enricoghiorzi parametricityfornestedtypesandgadts |