Верификация корректности музыки с помощью системы типов:
https://www.infoq.com/articles/type-systems-verifying-musical-correctness

TL;DR: музыкальные композиции могут быть проверены с помощью системы типов, чтобы сделать негармоничные переходы между нотами непредставимыми. Для этого используется библиотека для хаскеля Mezzo и приводятся примеры с завтипами на идрисе. «Корректность» музыки вообще расплывчатый термин, поэтому в статье применяется дескриптивный подход — «если музыкальная тема отклоняется от ожидаемой модели, то это необычно» — и построение матрицы энтропии для различных комбинаций переходов от ноты к ноте.