依存型付き音楽
https://prg.is.titech.ac.jp/ja/projects/typesystem/dependently-typed-music/