👰🏻 💅🏿 👩🏼‍✈️ Pemeriksaan sistem tipe untuk memeriksa kebenaran musik 🎐 🐨 👨‍👧‍👧

Saat ini, ada banyak pembicaraan tentang presentasi musik menggunakan bahasa pemrograman, karena di satu sisi itu adalah tugas yang menarik bagi para insinyur, dan di sisi lain itu adalah bagian dari deskripsi universal musik.

Seperti apa bentuknya? Untuk banyak bahasa, lingkungan pemrograman musik telah dibuat. Yang paling populer adalah TidalCycles for Haskell dan Sonic Pi untuk Ruby di Raspberry Pi. Ada juga alat menggunakan perpustakaan komposer Leipzig . Karena ini ditulis dalam Clojure, tidak memiliki pemeriksaan tipe.

(def row-row-row-your-boat
  (phrase [3/3 3/3 2/3 1/3 3/3]
          [  0   0   0   1   2]))

->> row-row-row-your-boat
  (canon (simple 4))
  (where :pitch (comp C major))
  (where :time (bpm 90))
  play)

Durasi dan nada suara direpresentasikan sebagai bilangan bulat dan koefisien literal, yang sangat tidak nyaman. Ketika datang ke transformasi musik, pemrograman bisa sangat membantu. Katakanlah, dalam contoh di atas, kunci diatur ke kunci C mayor dan tempo adalah 90 denyut per menit.

Ketika programmer melihat kode musik, mereka paling sering bertanya apakah mungkin untuk mencegah eksekusi palsu menggunakan sistem tipe. Pertanyaan yang adil. Jika musik dapat direpresentasikan sebagai kode, dapatkah kesalahan dalam menulis musik dianggap sebagai kesalahan pemrograman? Dan jika demikian, mengapa tidak meningkatkan proses menulis musik menggunakan teknik yang kita gunakan untuk menulis program?

Secara khusus, ada analogi yang jelas antara kesalahan bahwa sistem tipe dapat mencegah dan kasus umum ketidaktepatan musik. Jika bahasa pemrograman Anda dapat memeriksa apakah Anda meneruskan sebuah string ke fungsi yang mengharapkan untuk mendapatkan nomor, maka itu dapat memeriksa bahwa Anda tidak menggunakan f-sharp dalam suatu bagian yang ditulis dalam C mayor, kuncinya yang tidak ada tanda-tanda perubahan.

Pada artikel ini, kita akan menemukan apa yang membuat musik menjadi benar dan bagaimana cara merepresentasikannya menggunakan sistem tipe.

Preskriptifvisme

Para teoris telah berargumentasi selama berabad-abad tentang apa yang membuat musik menjadi benar. Paling sering, mereka beroperasi dalam kerangka preskriptifvisme musik: mengevaluasi musik untuk kepatuhan dengan sejumlah aturan.

Anda dapat menggambarkan metodologi dominan untuk pembentukan aturan:

Mempelajari kanon
Definisi pola
Merumuskannya sebagai seperangkat aturan

Maka dapat dikatakan bahwa:

Musik yang tidak mematuhi aturan ini salah.

Misalnya, aturan komposisi menyatakan bahwa tidak diperbolehkan untuk melompat ke septima besar dari ke ke dalam melodi. Pendekatan ini telah menghasilkan banyak temuan berharga. Musik klasik memiliki pola yang sangat menarik, dan generalisasi pengamatan kami sebagai seperangkat aturan membantu dalam membahas fenomena musik.

Selain itu, mengikuti aturan berguna saat menguasai alat musik. Ada baiknya ketika guru mengoreksi anak-anak yang berlatih bermain biola di C mayor, tetapi tersesat. Ada situasi di mana berguna untuk mematuhi definisi musik yang benar dan salah.

Namun, pendekatan ini memiliki dua kelemahan utama.

Pertama, aturan yang muncul dari proses ini sangat tergantung pada apa yang oleh teori dianggap kanon. Bias dataset mengarah ke bias kesimpulan, dan musik klasik Barat tidak mencerminkan keseluruhan pengalaman musik umat manusia. Membuat aturan berdasarkan musik Bach dan Mozart bisa menyenangkan, tetapi mereka tidak akan memberi tahu Anda terlalu banyak tentang musik secara umum.

Situasi menjadi rumit ketika Anda menyadari bahwa genre musik seringkali sangat terkait dengan budaya dan kelompok etnis tertentu, dan memprioritaskan jenis musik tertentu sehingga Anda tanpa sadar memprioritaskan jenis orang tertentu. Sebagai contoh, dalam teori akademis musik banyak perhatian diberikan pada studi tradisi Eropa klasik dan relatif sedikit untuk musik yang berasal dari diaspora imigran dari Afrika.: blues, jazz, rock and roll dan hip hop. Jika kita mengevaluasi kebenaran musik melalui teori tradisional, ini mungkin mengarah pada versi kultural masalah, ketika algoritma pengenalan wajah bekerja lebih baik dengan orang Kaukasia daripada dengan orang Negroid.

Kelemahan besar kedua dalam membuat aturan dengan mengidentifikasi dan menyamaratakan pola adalah bahwa dengan cara ini kita akan selalu fokus pada masa lalu. Dan musik paling menggairahkan ketika melanggar aturan. Sebelum Jimmy Page menggunakan efek distorsi , insinyur menganggap kliping sinyal selama amplifikasi sebagai cacat. Dan meskipun pola yang diungkapkan membantu untuk memahami musik modern, namun, mereka sama sekali tidak cocok untuk mengevaluasi musik masa depan.

Jenis sistem yang baik untuk musik harus menghindari jebakan preskripivisme yang dijelaskan. Seharusnya tidak didasarkan pada kriteria yang tidak dapat diterima atau subyektif untuk musik yang benar. Pada saat yang sama, mencoba membuat status yang salah tidak dapat ditampilkan , sistem tipe tidak boleh mengganggu penampilan negara baru.

Descriptivisme

Alternatif untuk prescriptivisme adalah descriptivisme. Jika dalam kasus pertama pola musik dianggap sebagai aturan yang mengikat, maka dalam pola kedua mereka dianggap sebagai pola yang terbentuk selama latihan. Pendekatan deskriptif untuk mempelajari aturan musik terlihat seperti ini:

Menjelajahi tubuh musik
Identifikasi tren
Kami merumuskannya dalam bentuk model

Dapat dikatakan bahwa:

Musik yang menyimpang dari model tidak biasa.

Untuk melakukan ini, kita memerlukan model struktur musik yang baik yang dapat menggambarkan yang biasa atau yang tidak biasa, daripada yang benar atau yang salah. David Huron, dalam bukunya Sweet Anticipation, menawarkan teori deskriptif yang dapat direduksi menjadi tiga aspek utama:

Musik dinilai melalui pelatihan statistik
Anda puas dengan perkiraan yang benar
Kebaruan tidak membuat Anda bosan

Dalam contoh preskripsi kami sebelumnya, melompat dari not ke C dianggap sebagai kesalahan. Dan menurut teori Huron, ini akan sangat tidak biasa. Mereka yang telah banyak mendengarkan musik Barat akan mengetahui bahwa ketika mereka mendengar not, maka not berikutnya akan lebih sering berupa not yang lain, atau not satu langkah lebih tinggi atau lebih rendah bunyinya. Melompat ke B akan mengejutkan penonton, dan mereka mungkin menganggapnya negatif.

Salah satu konsekuensi aneh dari teori Huron adalah bahwa menulis musik bukanlah latihan dalam memaksimalkan atau meminimalkan fiksi. Saldo musik di perbatasan antara ketertiban dan kekacauan, dan lokasi pendengar tergantung pada kemampuan musisi untuk menyeimbangkan kejutan kebaruan dengan kepuasan menerima yang diharapkan. Jika Anda benar-benar ingin memeriksa kebenaran komposisi, Anda harus memastikan bahwa itu tidak terlalu jauh dari tradisi yang diterima, tetapi tidak mengamatinya dengan terlalu ketat.

Berikut ini adalah data dari analisis statistik tren melodi. Warna yang lebih gelap menunjukkan hasil yang lebih mungkin. Pilih satu baris dengan salah satu catatan dan temukan di dalamnya sel dengan catatan yang lebih cenderung mengikuti yang Anda pilih - persimpangan disorot dalam gelap dengan kolom catatan lain. Sebagai contoh, dalam set data ini dalam 33,53% kasus setelah not kembali menjadi not.

Data ini diambil dari buku Huron, mereka adalah hasil analisis lebih dari 250.000 pasangan nada dari lagu-lagu rakyat Jerman di jurusan. Array data lain, misalnya hip-hop atau rock and roll, akan menunjukkan probabilitas yang berbeda.

Semua probabilitas ini dapat secara ekivalen direpresentasikan sebagai bit entropi: probabilitas 50% sesuai dengan satu bit, probabilitas 25% hingga dua bit, dll. Untuk menghindari pembagian dengan nol, kita mengasumsikan bahwa untuk transisi yang tidak pernah terjadi dalam dataset, probabilitasnya adalah 1/100 000. Sekarang warna yang lebih gelap menunjukkan transisi yang lebih mahal dalam hal entropi - yaitu, lebih kecil kemungkinannya. Sebagai contoh, untuk re setelah sama dengan 6 bit entropi, yaitu, ia memiliki probabilitas 1/64.

Representasi dalam bentuk entropi membantu kita untuk menggabungkan kejutan dari serangkaian catatan di mana setiap transisi dari satu suara ke yang lain adalah counter entropi, dengan kejutan dari keseluruhan melodi sebagai jumlah transisi.

 ->  ->  ->  = 2,20 + 2,71 + 5,94 = 10,85 
 ->  ->  ->  = 2,48 + 7,43 + 5,94 = 15,85

Ini sangat mirip dengan model Markov yang tersembunyi , tetapi alih-alih menghasilkan string not, kami menggunakan probabilitas tertimbang untuk memperkirakan kemungkinan melodi.

Anda mungkin telah memperhatikan bahwa transisi dari note ke C hanya 2,48 bit, walaupun pada pandangan pertama ini bertentangan dengan fakta bahwa transisi dari C ke C yang dijelaskan di atas sangat tidak biasa. Paling sering, transisi yang tidak biasa adalah sekitar 10 bit entropi. Alasan perbedaan adalah bahwa data Huron tidak membedakan antara lompatan enam not dari ke ke (sangat tidak biasa) dan transisi ke satu not dari ke ke lebih rendah (situasi yang cukup umum). Jika data memungkinkan kita untuk memisahkan kedua kasus ini, model akan menunjukkan bahwa rantai do-si-mi-fa akan terdengar lebih tidak konvensional daripada sebelumnya-re-mi-fa.

Catatan yang diketik

Idealnya, sistem tipe membantu programmer membuat keputusan yang tepat dan menghilangkan kemungkinan kesalahan. Analogi musikal yang baik adalah solfeggio. Jika Anda tidak memiliki pendidikan musik, maka Anda bisa berkenalan dengan solfeggio pada lagu Do-Re-Mi dari musikal The Sound of Music . Setiap nada oktaf memiliki namanya sendiri, dan nada apa pun di luar nada suara nama itu tidak memiliki:

Ke (catatan terendah dari set ini)
Kembali
Mi
F
Garam
La
Si
Ke (sekarang satu oktaf lebih tinggi)

Sistem ini memungkinkan musisi untuk mematuhi catatan yang benar, itu menetapkan bahasa mini yang melarang bermain catatan di luar tombol yang dipilih. Ada banyak sekali frekuensi antara d dan re, tetapi tidak direproduksi dalam solfeggio.

Ini dapat dengan mudah direpresentasikan dalam kode sebagai data tipe aljabar:

data Solfege = Do | Re | Mi | Fa | So | La | Ti

Sekarang Anda dapat menentukan fungsi musik yang tidak memungkinkan catatan di luar tombol. Misalnya, fungsi ini mengulangi satu nada dan beberapa kali:

repeat : Nat -> Solfege -> List Solfege
repeat 0 s = [s]
repeat n s = s :: repeat (n - 1) s

Dengan definisi ini, pengulangan tiga kali lipat dari note adalah ekspresi yang akan mudah dipahami dalam bidang musik. Pengulangan tiga kali lipat dari runcing tajam adalah kesalahan pemeriksaan tipe, karena runcing tajam bukan nilai tipe Solfege.

Ini memberi kita jenis keamanan tertentu. Sistem kami memungkinkan kami untuk menghindari not yang salah, tetapi tetap saja tidak melindungi terhadap kombinasi not yang salah. Jika kami bermain di C mayor, kami tidak akan bermain F tajam, tapi kami bisa bermain C, kemudian melompat ke septima besar pada not B, yang dilarang oleh aturan komposisi (tradisional). Pengecekan tipe kontekstual semacam itu dimungkinkan, tetapi membutuhkan pendekatan yang lebih kompleks.

Transisi yang diketik

Perpustakaan Mezzo Haskell menggunakan tipe terkait untuk memverifikasi kebenaran musik. Deskripsi mengatakan bahwa ini adalah "tes yang sangat ketat untuk musik", perpustakaan dapat memeriksa kepatuhan dengan berbagai aturan komposisi, dan bukan hanya nada suara. Di Mezzo, kode berikut dikompilasi karena melodi pra-re-mi-fa terdiri dari interval yang diizinkan:

comp = defScore $ start $ melody :| c :| d :| e :| f :>> g

Tetapi jika kita melanggar aturan yang melarang melompat dari ke ke si, maka Mezzo tidak akan mengkompilasi kode seperti itu:

comp = defScore $ start $ melody :| c :| b :| e :| f :>> g

Sangat menyenangkan bahwa Mezzo bahkan akan menunjukkan masalah:

Major sevenths are not permitted in melody: C and B
In the first argument of ‘(:|)’, namely ‘melody :| c :| b’
In the first argument of ‘(:|)’, namely ‘melody :| c :| b :| e’
In the first argument of ‘(:>>)’, namely
    ‘melody :| c :| b :| e :| f_’

Tampaknya mimpi menghadirkan musik yang salah sebagai kesalahan ketik telah menjadi kenyataan. Tetapi kadang-kadang situasi canggung muncul. Ketika penulis perpustakaan menyandikan pendahuluan Chopin, ternyata pada beberapa kesempatan komposer tidak mengikuti aturan tradisional:

Pekerjaan itu ditranskripsikan hampir seluruhnya, tetapi kadang-kadang perlu untuk melewatkan beberapa catatan, karena mereka menciptakan interval terlarang yang ditunjuk Mezzo.

Anda mungkin bertanya, siapa yang berjanji untuk melarangnya? Jika Chopin tidak diperbolehkan berbicara tentang apa yang diizinkan dalam musik Barat dan apa yang tidak, lalu siapa lagi?

Masalahnya adalah bahwa meskipun Mezzo mampu memperhitungkan konteks, estimasi tipe tetap menjadi tugas pilihan biner. Entah semua catatan itu benar dan pekerjaan dikompilasi, apakah salah satu catatan itu pingsan dan pekerjaan itu tidak dikompilasi. Dan terlepas dari kenyataan bahwa Mezzo memungkinkan Anda memilih aturan komposisi, keputusan untuk menerapkan atau tidak menerapkan aturan tersebut bersifat global. Jika Anda menonaktifkan aturan karena beberapa keputusan musik melanggar perjanjian yang biasa, maka Anda akan membatalkan pemeriksaan bagian lain dari karya tersebut.

Entropi yang diketik

Salah satu cara untuk melanggar atau menghindari aturan pengetikan musik adalah dengan memodelkan transisi di antara catatan dalam hal kesamaan pada saran Huron. Alih-alih menyatakan transisi tertentu benar atau salah, Anda dapat menghitung jumlah entropi yang mencerminkan kejutan penonton pada kombinasi pasangan catatan.

Kode berikut ini ditulis dalam Idris bahasa fungsional yang diketik tergantung . Dalam kode, diperiksa bahwa melodi yang sesuai dengan aturan dimulai dari dan diakhiri dengan garam dan bahwa jalur di antara not-not ini menghasilkan 8-16 bit entropi. Pertama, Anda perlu menentukan jenis Melodyyang mencerminkan representasi melodi kami dengan kesamaan atau besarnya entropi tertentu. Tipe ini memiliki tiga konstruktor:

Pure: Mencerminkan penciptaan melodi dari satu not, dengan level entropi atas dan bawah sama dengan nol.
(>>=): mengambil dua melodi dan menambahkan batas entropi mereka dengan biaya beralih dari nada di akhir melodi pertama ke nada di akhir nada kedua.
Relax: mengambil melodi dan memperluas batas-batas entropinya.

data Melody : (Solfege, Solfege) -> (Nat, Nat) -> Type where

  Pure  : x -> Melody (x, x) (0, 0)

  (>>=) : Melody (w, x) (low, high) ->
          (() -> Melody (y, z) (low2, high2)) ->
          Melody (w, z) (cost x y + low + low2, cost x y + high + high2)

  Relax : Melody (x, y) (low + dl, high) ->
          Melody (x, y) (low, high + dh)

Definisi jenis ini lebih rumit, tetapi berkat itu, Idris dapat membuat melodi menggunakan notasi do, dan kompiler akan melacak batasan entropi untuk kita. Inilah nada yang relevan dengan biaya rendah dari semua transisi:

conventional : Melody (Do, So) (8, 16)
conventional = Relax $ do
  Pure Do
  Pure Re
  Pure Mi
  Pure Fa
  Pure So

Lagu berikut ini tidak sesuai dengan aturan, karena ia melompat ke septima besar. Di Mezzo, itu akan dilarang, atau Anda harus menonaktifkan aturan sepenuhnya. Di sini kami hanya memperluas batas kompleksitas melodi sehingga sesuai dengan kisaran 8-24 bit entropi:

unconventional : Melody (Do, So) (8, 24)
unconventional = Relax $ do
  Pure Do
  Pure Ti
  Pure Mi
  Pure Fa
  Pure So

Jika sebaliknya Melody (Do, So) (8, 24)kami akan menetapkan jenis yang tidak sesuai dengan aturan melodi Melody (Do, So) (8, 16), maka itu tidak akan dikompilasi!

Kebaruan dari pendekatan ini adalah memungkinkan Anda untuk memahami ketika musik menjadi terlalu membosankan. Jika entropi melodi tidak mencapai batas bawah, kesalahan jenis akan muncul. Jadi jika Anda menetapkan jenis melodi yang sesuai dengan aturan, Melody (Do, So) (16, 24)maka tidak akan dikompilasi juga, karena entropinya tidak mencapai batas bawah. Ini mengilhami kami dengan keyakinan pada teori Huron, yang menurutnya akan terlalu sulit bagi orang untuk mendengarkan musik yang terlalu tidak biasa atau tidak dapat diprediksi.

Dalam kasus degenerasi, transisi antara catatan di dalam kunci tidak meningkatkan entropi, dan transisi di luar kunci memberikan peningkatan besar dalam entropi secara sewenang-wenang. Maka disarankan untuk kembali ke evaluasi biner, di mana setiap not akan dianggap diizinkan atau dilarang, tanpa status perantara.

Penting tetapi sulit diverifikasi

Memeriksa jenis-jenis musik itu sulit karena sulit untuk menentukan kebenaran musik. Jika kita tidak dapat secara matematis memodelkan definisi dari kebenaran musik, maka kita tidak dapat mentransfernya ke sistem tipe. Bahkan jika kita dapat secara formal memformalkan pemahaman kita, kita perlu melakukan upaya dan menerapkan sistem tipe yang kuat sehingga kompiler dapat mengevaluasi melodi secara memadai. Namun, ini dimungkinkan dengan beberapa definisi dan beberapa asumsi penyederhanaan.

Apakah ini hanya rasa ingin tahu? Mungkin. Tidak mungkin bahwa industri musik akan segera mengadopsi sistem tipe untuk mencegah kesalahan komposisi. Tetapi jika studi komputasi dalam bidang musik akan membantu kita untuk mengevaluasi secara berbeda apa yang memainkan peran penting dalam kehidupan kita semua, maka ini saja membenarkan semua upaya.

Mungkin yang tidak kalah penting adalah kenyataan bahwa musik hanyalah salah satu bidang di mana kebenaran itu penting, tetapi sulit untuk diverifikasi. Semakin aktif lingkup sosial dan budaya terotomatisasi dengan bantuan pemrograman, semakin sering situasi muncul di mana sulit untuk mengevaluasi jawabannya, yang sangat penting bagi orang-orang. Ambil penggunaan program komputer yang memutuskan berapa lama untuk dipenjara . Ketepatan kalimat yang dijatuhkan tergantung pada kompromi yang rumit antara biaya dan probabilitas, dan jika kita tidak dapat melacak logika pengambilan keputusan oleh sistem, lalu bagaimana kita bisa mengevaluasi keadilan hasil?

Setiap kali kita mengotomatiskan proses pengambilan keputusan yang buram, kita perlu bertanya pada diri sendiri: "Bagaimana kita tahu bahwa sistem bekerja dengan benar?"