Dependently Typed Music

In programming languages, we use typing rules to write programs that make sense.  In music theory, on the other hand, we use composition rules to create music that sound good.  This correspondence motivates us to investigate typed music composition, where composition rules are represented as typing rules, and violation of rules are reported as type errors.

We develop Music Tools, a library of musical tools written in Agda.  The idea is to use Agda’s dependent types to concisely express various composition rules, while using Haskell’s support for music generation via the foreign function interface.

Members

News