2019/03/19 by Chris Jenkins, Jenkins, Christopher, Colin McDonald +3
Computer Science · #68N15 #FOS: Computer and information sciences #Logic, programming, and type systems #Numerical Methods and Algorithms #Parallel Computing and Optimization Techniques #Programming Languages (cs.PL)
paper · pdf · doi:10.48550/arxiv.1903.08233
openalex publication_date 2019/03/19 · openalex created_date 2022/07/29 · openalex updated_date 2026/07/28
In the Calculus of Dependent Lambda Eliminations (CDLE), a pure Curry-style\ntype theory, it is possible to generically \λ-encode inductive datatypes\nwhich support course-of-values (CoV) induction. We present a datatype subsystem\nfor Cedille (an implementation of CDLE) that provides this feature to\nprogrammers through convenient notation for declaring datatypes and for\ndefining functions over them by case analysis and fixpoint-style recursion\nguarded by a type-based termination checker. We demonstrate that this does not\nrequire extending CDLE by showing how datatypes and functions over them\nelaborate to \λ-encodings, and proving that this elaboration is type-\nand value-preserving. This datatype subsystem and elaborator are implemented in\nCedille, establishing for the first time a complete translation of inductive\ndefinitions to a small pure typed \λ-calculus.\n