Print Email Facebook Twitter Replication and formalization of (Co)Church encoded shortcut fusion Title Replication and formalization of (Co)Church encoded shortcut fusion: Master's Thesis Author Rogers, Eben (TU Delft Electrical Engineering, Mathematics and Computer Science) Contributor Poulsen, C.B. (mentor) Reinders, J.S. (mentor) Cockx, J.G.H. (mentor) Hai, R. (graduation committee) Degree granting institution Delft University of Technology Programme Computer Science | Software Technology Date 2024-06-24 Abstract When writing functional code that composes multiple recursive functions that operate on a datastrcuture, we often incur a lot of computational overhead allocating memory, only to later read, use, and discard this information.This can be alleviated using fusion, a technique that combines these multiple recursive datastructure traversals into one.This thesis explores shortcut fusion using (Co)Church encodings based on the work of Harper (2011), focusing on two questions: What is needed to reliably achieve fusion in Haskell, and the correctness of these transformations through a formalization in Agda.The first contribution replicates and extends Harper's (Co)Church encodings in Haskell, uncovering optimizer weaknesses and providing practical insights for achieving fusion within Haskell.The second contribution formalizes these encodings in Agda, leveraging parametricity and the category theory described by Harper.The formalization proves the equivalence of these encoded functions to the unencoded ones, showing that the encodings are in fact isomorphisms, as long as parametricity (Wadler, 1989) is assumed.These findings highlight the effectiveness and correctness of shortcut fusion techniques and show the promise of shortcut fusion: Reduce the computational overhead associated with functional programming while retaining its nice, compositional properties. Subject FusionShortcut fusionCategory TheoryFoldBuildUnfoldDestroyHaskellAgdaReflectionParametricityFree theoremDeforestationFormal verificationFunctional programmingContainersContainerCatamorphismCatamorphismsAnamorphismAnamorphismsStricly positive functorFormalizationIsomorphismFoldrUnfoldrBisimilarityBisimulationInitial objectsTerminal objectsType systemDependent type theoryDependent typesFormal proofProgramming languages To reference this document use: http://resolver.tudelft.nl/uuid:7474b56a-345c-42b7-8d07-e7163d1bde05 Bibliographical note https://github.com/Bigstep22/thesis Repository link The link to the repository in which my work was done. This contains the same data as the artifacts. Part of collection Student theses Document type master thesis Rights © 2024 Eben Rogers Files PDF main.pdf 1.78 MB Close viewer /islandora/object/uuid:7474b56a-345c-42b7-8d07-e7163d1bde05/datastream/OBJ/view