|
Journal of Functional Programming
Journal Prestige (SJR): 0.458  Citation Impact (citeScore): 1 Number of Followers: 1  Hybrid journal (It can contain Open Access articles)ISSN (Print) 0956-7968 - ISSN (Online) 1469-7653 Published by Cambridge University Press  [353 journals]
|
- Is sized typing for Coq practical'
-
Free pre-print version: Loading...
Authors: CHAN; JONATHAN, LI, YUFENG, BOWMAN, WILLIAM J.
First page: 1
Abstract: Contemporary proof assistants such as Coq require that recursive functions be terminating and corecursive functions be productive to maintain logical consistency of their type theories, and some ensure these properties using syntactic checks. However, being syntactic, they are inherently delicate and restrictive, preventing users from easily writing obviously terminating or productive functions at their whim.Meanwhile, there exist many sized type theories that perform type-based termination and productivity checking, including theories based on the Calculus of (Co)Inductive Constructions (CIC), the core calculus underlying Coq. These theories are more robust and compositional in comparison. So why haven’t they been adapted to Coq'In this paper, we venture to answer this question with CIC
, a sized type theory based on CIC. It extends past work on sized types in CIC with additional Coq features such as global and local definitions. We also present a corresponding size inference algorithm and implement it within Coq’s kernel; for maximal backward compatibility with existing Coq developments, it requires no additional annotations from the user.In our evaluation of the implementation, we find a severe performance degradation when compiling parts of the Coq standard library, inherent to the algorithm itself. We conclude that if we wish to maintain backward compatibility, using size inference as a replacement for syntactic checking is impractical in terms of performance.
PubDate: 2023-01-24
DOI: 10.1017/S0956796822000120
-
- Folding left and right matters: Direct style, accumulators, and
continuations-
Free pre-print version: Loading...
Authors: DANVY; OLIVIER
First page: 2
Abstract: The equivalence of folding left and right over Peano numbers and lists makes it possible to minimalistically inter-derive (1) structurally recursive functions in direct style, (2) structurally tail-recursive functions that use an accumulator, and (3) structurally tail-recursive functions in delimited continuation-passing style, using Ohori and Sasano’s lightweight fusion by fixed-point promotion. When the fold-left and the fold-right functions account for primitive iteration for Peano numbers, this equivalence is unconditional. When they account for primitive recursion for Peano numbers, this equivalence is modulo left permutativity of their induction-step parameter – a property which is more general than associativity and commutativity. And when they account for primitive iteration or for primitive recursion over lists, this equivalence is modulo left permutativity of their induction-step parameter if these two fold functions have the same type. Since the 1980s, however, the two fold functions for lists do not have the same type: the arguments for their induction-step parameter are swapped, a re-ordering that complicated Bird and Wadler’s duality theorems and whose history is reviewed in an appendix. Without this re-ordering, Bird and Wadler’s second duality theorem more visibly accounts for “re-bracketing,” which is a key step to make recursive programs tail recursive in the general area of program development, from Cooper in the 1960s and onwards.
PubDate: 2023-02-14
DOI: 10.1017/S0956796822000156
-
- Fold-unfold lemmas for reasoning about recursive programs using the Coq
proof assistant – ERRATUM-
Free pre-print version: Loading...
Authors: DANVY; OLIVIER
First page: 3
PubDate: 2023-03-06
DOI: 10.1017/S0956796823000011
-
- Classical (co)recursion: Mechanics
-
Free pre-print version: Loading...
Authors: DOWNEN; PAUL, ARIOLA, ZENA M.
First page: 4
Abstract: Recursion is a mature, well-understood topic in the theory and practice of programming. Yet its dual, corecursion is underappreciated and still seen as exotic. We aim to put them both on equal footing by giving a foundation for primitive corecursion based on computation, giving a terminating calculus analogous to the original computational foundation of recursion. We show how the implementation details in an abstract machine strengthens their connection, syntactically deriving corecursion from recursion via logical duality. We also observe the impact of evaluation strategy on the computational complexity of primitive (co)recursive combinators: call-by-name allows for more efficient recursion, but call-by-value allows for more efficient corecursion.
PubDate: 2023-04-04
DOI: 10.1017/S0956796822000168
-
- Read/write factorizable programs
-
Free pre-print version: Loading...
Authors: BHASKAR; SIDDHARTH, SIMONSEN, JAKOB GRUE
First page: 5
Abstract: In the cons-free programming paradigm, we eschew constructors and program using only destructors. Cons-free programs in a simple first-order language with string data capture exactly P, the class of polynomial-time relations. By varying the underlying language and considering other data types, we can capture several other complexity classes. However, no cons-free programming language captures any functional complexity class for fundamental reasons. In this paper, we cleanly extend the cons-free paradigm to encompass functional complexity classes. Namely, we introduce programs with data that can either only be destructed or only be constructed, which we enforce by a type system on the program variables. We call the resulting programs read/write- (or RW-)factorizable, show that RW-factorizable string programs capture exactly the class FP of polynomial-time functions, and that tail-recursive RW-factorizable programs capture exactly the class FL of logarithmic-space functions. Finally, we state and solve the nontrivial problem of syntactic composition of two RW-factorizable programs.
PubDate: 2023-06-08
DOI: 10.1017/S0956796823000023
-
