APLAS 2024
Tue 22 - Fri 25 October 2024 Kyoto

What if we could assemble data-types by first picking a recursive structure and then grafting data at selected locations, according to a well-defined blueprint? What if, moreover, this underlying structure had a straightforward semantics in terms of the number of elements it can support? This is the promise of Okasaki’s numerical representations.

This paper offers a journey from Electronic Engineering —computing with binary numbers— to Functional Programming —implementing a persistent random-access list datatype— guided by the type-theoretic framework of McBride’s ornaments.