A well-known representation of monoids and its application to the function 'vector reverse'. (8th August 2022)

• Record Type: Journal Article
• Authors: SWIERSTRA, WOUTER
• Is Part Of: Journal of functional programming. Volume 32(2022)
• Publication Date: 2022-08-08
• Subjects: Functional programming (Computer science) -- Periodicals
• DOI: 10.1017/S0956796822000065
• Languages: English
• ISSNs: 0956-7968

Abstract

Abstract: Vectors—or length-indexed lists—are classic example of a dependent type. Yet, most tutorials stay clear of any function on vectors whose definition requires non-trivial equalities between natural numbers to type check. This pearl shows how to write functions, such as vector reverse, that rely on monoidal equalities to be type correct without having to write any additional proofs. These techniques can be applied to many other functions over types indexed by a monoid, written using an accumulating parameter, and even be used to decide arbitrary equalities over monoids 'for free.'