Build, Augment and Destroy, Universally

Abstract. We give a semantic footing to the fold/build syntax of programming with inductive types, covering shortcut deforestation, based on a universal property. Specifically, we give a semantics for inductive types based on limits of algebra structure forgetting functors and show that it is equivalent to the usual initial algebra semantics. We also give a similar semantic account of the augment generalization of build and of the unfold/destroy syntax of coinductive types.

• Type: Conference
• Year: 2004
• Where: APLAS
• Authors: Neil Ghani, Tarmo Uustalu, Varmo Vene
• Keywords: APLAS 2004, Inductive Types, Initial Algebra Semantics, Structure Forgetting Functors