More Like this

1. Parametricity for Primitive Nested Types

   https://doi.org/10.26226/morressier.604907f41a80aac83ca25cb5  

   Johann, P; Ghiorzi, E.; Jeffries, D. (January 2021, Lecture notes in computer science)

   Kiefer, S; Tasson, C. (Ed.)

   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 cocontinuity 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. 

   more » « less
2. GADTs, Functoriality, Parametricity: Pick Two

   Johann, P.; Ghiorzi, E.; and Jeffries, D. (January 2021, Logical And Semantic Frameworks with Applications)

   null (Ed.)

   GADTs can be represented either as their Church encodings a la Atkey, or as fixpoints a la Johann and Polonsky. While a GADT represented as its Church encoding need not support a map function satisfying the functor laws, the fixpoint representation of a GADT must support such a map function even to be well-defined. The two representations of a GADT thus need not be the same in general. This observation forces a choice of representation of data types in languages supporting GADTs. In this paper we show that choosing whether to represent data types as their Church encodings or as fixpoints determines whether or not a language supporting GADTs can have parametric models. This choice thus has important consequences for how we can program with, and reason about, these advanced data types. 

   more » « less
3. GADTs, Functoriality, Parametricity: Pick Two

   https://doi.org/10.4204/EPTCS.357.6  

   Johann, Patricia; Ghiorzi, Enrico; Jeffries, Daniel (January 2021, Logical and Semantic Frameworks with Applications)

   GADTs can be represented either as their Church encodings a la Atkey, or as fixpoints a la Johann and Polonsky. While a GADT represented as its Church encoding need not support a map function satisfying the functor laws, the fixpoint representation of a GADT must support such a map function even to be well-defined. The two representations of a GADT thus need not be the same in general. This observation forces a choice of representation of data types in languages supporting GADTs. In this paper we show that choosing whether to represent data types as their Church encodings or as fixpoints determines whether or not a language supporting GADTs can have parametric models. This choice thus has important consequences for how we can program with, and reason about, these advanced data types. 

   more » « less
4. (Deep) Induction Rules for GADTs

   https://doi.org/10.1145/3497775.3503680  

   Johann, Patricia; Ghiorzi, Enrico (January 2022, Certified Proofs and Programs)

   Deep data types are those that are constructed from other data types, including, possibly, themselves. In this case, they are said to be truly nested. Deep induction is an extension of structural induction that traverses all of the structure in a deep data type, propagating predicates on its primitive data throughout the entire structure. Deep induction can be used to prove properties of nested types, including truly nested types, that cannot be proved via structural induction. In this paper we show how to extend deep induction to GADTs that are not truly nested GADTs. This opens the way to incorporating automatic generation of (deep) induction rules for them into proof assistants. We also show that the techniques developed in this paper do not suffice for extending deep induction to truly nested GADTs, so more sophisticated techniques are needed to derive deep induction rules for them. 

   more » « less
5. Early Announcement: Parametricity for GADTs

   Cagne, Pierre; Johann, Patricia (June 2024, Mathematical Foundations of Program Semantics 2024)

   Relational parametricity was first introduced by Reynolds for System F. Although System F provides a strong model for the type systems at the core of modern functional programming languages, it lacks features of daily programming practice such as complex data types. In order to reason parametrically about such objects, Reynolds’ seminal ideas need to be generalized to extensions of System F. Here, we explore such a generalization for the extension of System F by Generalized Algebraic Data Types (GADTs) as found in Haskell. Although GADTs generalize Algebraic Data Types (ADTs) — i.e., simple recursive types such as lists, trees, etc. — we show that naively extending the parametric treatment of these recursive types is not enough to tackle GADTs. We propose a tentative workaround for this issue, borrowing ideas from the categorical semantics of GADTs known as “functorial completion”. We discuss some applications, as well as some limitations, of this solution. 

   more » « less