Well-typed music does not sound wrong (experience report)

D Szamozvancev, MB Gale - Proceedings of the 10th ACM SIGPLAN …, 2017 - dl.acm.org
Proceedings of the 10th ACM SIGPLAN International Symposium on Haskell, 2017dl.acm.org
Music description and generation are popular use cases for Haskell, ranging from live
coding libraries to automatic harmonisation systems. Some approaches use probabilistic
methods, others build on the theory of Western music composition, but there has been little
work done on checking the correctness of musical pieces in terms of voice leading,
harmony, and structure. Haskell's recent additions to the type-system now enable us to
perform such analysis statically. We present our experience of implementing a type-level …
Music description and generation are popular use cases for Haskell, ranging from live coding libraries to automatic harmonisation systems. Some approaches use probabilistic methods, others build on the theory of Western music composition, but there has been little work done on checking the correctness of musical pieces in terms of voice leading, harmony, and structure. Haskell's recent additions to the type-system now enable us to perform such analysis statically.
We present our experience of implementing a type-level model of classical music and an accompanying EDSL which enforce the rules of classical music at compile-time, turning composition mistakes into compiler errors. Along the way, we discuss the strengths and limitations of doing this in Haskell and demonstrate that the type system of the language is fully capable of expressing non-trivial and practical logic specific to a particular domain.
ACM Digital Library