Weighted Refinement Types for Counterpoint Composition

Refinement types are useful for describing specifications of programs. When applied to music theory, however, refinement types are too restrictive in that they do not allow breaking of rules. To relax this restriction, we propose weighted refinement types, a variation of refinement types where each refinement predicate carries a weight representing the importance of that predicate. In this paper, we present a weighted refinement type system that has core features required for composing species counterpoint. We also discuss potential applications of weighted refinement types in non-musical domains.