Western music of the common practice period tends to loosely follow sets of rules, which were developed over time to ensure the aesthetic quality of the composition. To help analyze and synthesize tonal music, it is worthwhile to encode these rules into a programming language. As shown by recent studies, functional programming languages are particularly suited to this task.

We present Music Tools, a library of small tools that can be combined functionally to help analyze and synthesize music. To allow simple and natural encoding of rules, we built the library in Agda, which is a functional language with full dependent types. As an application of the library, we demonstrate an implementation of species counterpoint. We show how Agda’s rich type system enables us to express required rules, and helps both human and computers compose correct counterpoint.