依存型付き音楽

プログラミング言語では、意味をなすプログラムを書くために型規則を用います。一方、音楽理論では、響きの良い音楽を作るために作曲規則を用います。この対応関係から、型付き音楽の生成という発想が生まれます。つまり、音楽の規則を型規則として表現し、規則の違反を型エラーとして報告する、という考え方です。

このプロジェクトでは、音楽生成のためのライブラリ Music Tools を、Agda 言語で実装します。アイディアとしては、Agda の依存型を用いてさまざまな作曲規則を簡潔に表現しつつ、FFI を通して Haskell の音楽生成機能を利用します。

メンバー