Logo image
Back
Monotone recursive types and recursive data representations in Cedille
Journal article   Open access   Peer reviewed

Monotone recursive types and recursive data representations in Cedille

Christopher Jenkins and Aaron Stump
Mathematical structures in computer science, Vol.31(6), pp.1-64
12/10/2021
DOI: 10.1017/S0960129521000402
Appears in  UI Libraries Support Open Access
url
https://doi.org/10.1017/S0960129521000402View
Published (Version of record) Open Access

Abstract

Abstract Guided by Tarksi’s fixpoint theorem in order theory, we show how to derive monotone recursive types with constant-time roll and unroll operations within Cedille, an impredicative, constructive, and logically consistent pure typed lambda calculus. This derivation takes place within the preorder on Cedille types induced by type inclusions, a notion which is expressible within the theory itself. As applications, we use monotone recursive types to generically derive two recursive representations of data in lambda calculus, the Parigot and Scott encoding. For both encodings, we prove induction and examine the computational and extensional properties of their destructor, iterator, and primitive recursor in Cedille. For our Scott encoding in particular, we translate into Cedille a construction due to Lepigre and Raffalli (2019) that equips Scott naturals with primitive recursion, then extend this construction to derive a generic induction principle. This allows us to give efficient and provably unique (up to function extensionality) solutions for the iteration and primitive recursion schemes for Scott-encoded data.
 UIOWA OA Agreement

Details

Metrics

22 Record Views
Logo image