Exame do sistema de tipos para verificar a exatidão da música



Hoje, fala-se muito sobre a apresentação de música usando linguagens de programação, porque, por um lado, é uma tarefa interessante para os engenheiros e, por outro, faz parte da descrição universal da música.

Com o que se parece? Para muitos idiomas, os ambientes de programação musical foram criados. Os mais populares são TidalCycles for Haskell e Sonic Pi for Ruby no Raspberry Pi. Há também uma ferramenta usando a biblioteca do compositor de Leipzig . Como está escrito em Clojure, falta verificação de tipo.

(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)

A duração e o tom dos sons são representados como números inteiros e coeficientes literais, o que não é muito conveniente. Quando se trata de transformação musical, a programação pode ser uma grande ajuda. Digamos, no exemplo acima, a tecla está definida como C maior e o tempo é de 90 batimentos por minuto.

Quando os programadores veem o código da música, na maioria das vezes perguntam se é possível impedir a execução falsa usando um sistema de tipos. Questão justa. Se a música pode ser representada como código, os erros na composição podem ser considerados erros de programação? E se sim, por que não melhorar o processo de escrever músicas usando as técnicas que usamos para escrever programas?

Em particular, existe uma analogia óbvia entre erros que o sistema de tipos pode impedir e casos comuns de imprecisão musical. Se sua linguagem de programação conseguir verificar se você passou uma string para uma função que espera obter um número, poderá verificar se você não usa f-sharp em uma passagem escrita em Dó maior, cuja chave não há sinais de alteração.

Neste artigo, descobriremos o que torna a música correta e como ela pode ser representada usando um sistema de tipos.

Prescritivismo


Os teóricos vêm discutindo há séculos sobre o que torna a música certa. Na maioria das vezes, eles operam dentro da estrutura do prescritivismo musical: avaliando a música quanto à conformidade com algum conjunto de regras.

Você pode descrever a metodologia dominante para a formação de regras:

  • Aprendendo o cânone
  • Definição de padrões
  • Formulando-os como um conjunto de regras

Então, pode-se argumentar que:

A música que não cumpre essas regras está incorreta.

Por exemplo, a regra de composição declara que não é permitido saltar para um septo grande de para s na melodia. Essa abordagem levou a inúmeras descobertas valiosas. A música clássica possui padrões extremamente interessantes, e uma generalização de nossas observações como um conjunto de regras ajuda a discutir o fenômeno da música.

Além disso, é útil seguir as regras ao dominar instrumentos musicais. É bom quando os professores corrigem as crianças que praticam violino em Dó maior, mas se desviam. Há situações em que é útil aderir às definições de música correta e incorreta.

No entanto, essa abordagem tem duas principais desvantagens.

Primeiro, as regras decorrentes desse processo são altamente dependentes daquilo que o teórico considera cânone. O viés do conjunto de dados leva ao viés das conclusões, e a música clássica ocidental não reflete toda a experiência musical da humanidade. Criar regras baseadas nas músicas de Bach e Mozart pode ser divertido, mas elas não falam muito sobre música em geral.

A situação é complicada quando você percebe que os gêneros musicais geralmente estão fortemente associados a certas culturas e grupos étnicos e que, ao priorizar certos tipos de música, você prioriza inconscientemente certos tipos de pessoas. Por exemplo, na teoria acadêmica da música, muita atenção é dada ao estudo das tradições clássicas européias e relativamente pouca música originada nas diásporas de imigrantes da África: blues, jazz, rock and roll e hip hop. Se avaliarmos a correção da música através de uma teoria tradicional, isso pode levar a uma versão culturológica do problema, quando os algoritmos de reconhecimento de faces funcionaram melhor com caucasianos do que com negróides.

A segunda grande desvantagem da criação de regras, identificando e generalizando padrões, é que, dessa maneira, sempre focaremos no passado. E a música se excita mais quando quebra as regras. Antes de Jimmy Page usar o efeito de distorção , os engenheiros consideraram o corte do sinal durante a amplificação como um defeito. E, embora os padrões revelados ajudem a entender a música moderna, eles são completamente inadequados para avaliar músicas futuras.

Um bom sistema de tipos de música deve evitar as duas armadilhas descritas de prescritivismo. Não deve ser baseado em critérios inaceitáveis ​​ou subjetivos para a música correta. Ao mesmo tempo, tentando tornar estados errôneos irrepresentáveis , o sistema de tipos não deve interferir no aparecimento de novos estados.

Descritivismo


Uma alternativa ao prescritivismo é o descritivismo. Se, no primeiro caso, os padrões musicais são considerados regras vinculativas, no segundo eles são considerados padrões formados no curso da prática. Uma abordagem descritiva para o estudo das regras musicais é assim:

  • Explorando o corpo da música
  • Identificar tendências
  • Nós os formulamos na forma de um modelo

Pode-se argumentar que:

A música que se desvia do modelo é incomum.

Para fazer isso, precisamos de um bom modelo de estruturas musicais que descreva o comum ou o incomum, e não o certo ou o errado. David Huron, em seu livro Sweet Anticipation, oferece uma teoria descritiva que pode ser reduzida a três aspectos principais:

  • A música é classificada através de treinamento estatístico
  • Você está satisfeito com a previsão correta
  • Novidade não deixa você ficar entediado

Em nosso exemplo prescritivista anterior, pular de uma nota para C é considerado um erro. E, de acordo com a teoria de Huron, isso será muito incomum. Aqueles que ouviram muita música ocidental descobrirão que, quando ouvirem uma nota, a próxima nota será com mais freqüência, ou uma nota um passo mais alto ou mais baixo. Saltar para o B surpreenderá o público, e eles podem encarar isso negativamente.

Uma das conseqüências curiosas da teoria de Huron é que escrever música não é um exercício para maximizar ou minimizar a ficção. A música se equilibra na fronteira entre ordem e caos, e a localização dos ouvintes depende da capacidade do músico de equilibrar o choque da novidade com a satisfação de receber o esperado. Se você realmente deseja verificar a exatidão da composição, precisará garantir que ela não vá muito longe das tradições aceitas, mas também não as observe estritamente.

A seguir, são apresentados dados de uma análise estatística de tendências melódicas. Cores mais escuras indicam resultados mais prováveis. Selecione uma linha com uma das notas e encontre nela uma célula com uma nota com maior probabilidade de seguir sua escolha - o cruzamento destacado em escuro com a coluna de outra nota. Por exemplo, neste conjunto de dados em 33,53% dos casos após a nota remetida à nota.


Estes dados são retirados do livro de Huron, são o resultado da análise de mais de 250.000 pares de tons de canções folclóricas germânicas em sua maioria. Outra matriz de dados, digamos, hip-hop ou rock and roll, demonstrará probabilidades diferentes.

Todas essas probabilidades podem ser representadas equivalentemente como bits de entropia: uma probabilidade de 50% corresponde a um bit, uma probabilidade de 25% a dois bits, etc. Para evitar a divisão por zero, assumimos que para transições que nunca ocorrem no conjunto de dados, a probabilidade é de 1/100 000. Agora, a cor mais escura mostra transições que são mais caras em termos de entropia - ou seja, menos provável. Por exemplo, para re after é igual a 6 bits de entropia, ou seja, tem uma probabilidade de 1/64.


A representação na forma de entropia nos ajuda a combinar surpresa de uma série de notas nas quais cada transição de um som para outro é um contador de entropia, com surpresa de toda a melodia como a soma das transições.

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

Isso é muito semelhante ao modelo oculto de Markov , mas, em vez de gerar sequências de notas, usamos probabilidades ponderadas para estimar a probabilidade de uma melodia.

Você deve ter notado que a transição da nota para C é de apenas 2,48 bits, embora à primeira vista isso contradiga o fato de que a transição de C para C foi descrita acima como muito incomum. Na maioria das vezes, transições incomuns são aproximadamente 10 bits de entropia. A razão para a discrepância é que os dados do Huron não distinguem entre um salto de seis notas de para para si (muito incomum) e uma transição para uma nota de para um si mais baixo (uma situação bastante comum). Se os dados nos permitirem separar esses dois casos, o modelo mostrará que a cadeia pré-si-mi-fa soará ainda mais não convencional do que a pré-re-mi-fa.

Notas digitadas


Idealmente, um sistema de tipos ajuda os programadores a tomar as decisões corretas e elimina a possibilidade de erros. Uma boa analogia musical é o solfejo. Se você não tem educação musical, pode se familiarizar com solfeggio na música Do-Re-Mi do musical The Sound of Music . Cada nota de uma oitava tem seu próprio nome e qualquer nota fora da tonalidade do nome não possui:

  1. Para (nota mais baixa deste conjunto)
  2. Mi
  3. F
  4. Sal
  5. La
  6. Si
  7. Para (agora uma oitava acima)

Este sistema permite que os músicos sigam as notas corretas, define um mini-idioma que proíbe tocar notas fora da tecla selecionada. Existem infinitas frequências entre d e re, mas elas não são reproduzidas no solfeggio.

Isso pode ser facilmente representado no código como dados do tipo algébrico:

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

Agora você pode definir funções musicais que não permitem notas fora das teclas. Por exemplo, esta função repete uma nota n vezes:

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

Com esta definição, a repetição tripla de uma nota re é uma expressão que será facilmente compreendida no campo musical. Uma repetição tripla de uma nitidez acentuada é um erro de verificação de tipo, porque a nitidez acentuada não é um valor de tipo Solfege.

Isso nos dá um certo tipo de segurança. Nosso sistema nos permite evitar as notas erradas, mas ainda não protege contra combinações incorretas de notas. Se tocássemos em Dó maior, não tocaríamos F nítido, mas poderíamos tocar C, depois pularemos para um septo grande em uma nota B, que é proibida pelas regras de composição (tradicionais). Essa verificação de tipo contextual é possível, mas requer uma abordagem mais complexa.

Transições digitadas


A biblioteca Mezzo Haskell usa tipos relacionados para verificar a correção musical. A descrição diz que este é um "teste muito estrito para a música", a biblioteca pode verificar a conformidade com várias regras de composição, e não apenas a tonalidade. No Mezzo, o código a seguir é compilado porque a melodia pre-re-mi-fa consiste nos intervalos permitidos:

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

Mas se violarmos a regra que proíbe saltar de para para si, o Mezzo não compilará esse código:

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

É ótimo que Mezzo até aponte um problema:

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_’

Pode parecer que o sonho de apresentar músicas incorretas como erros de digitação se tornou realidade. Mas às vezes surgem situações embaraçosas. Quando o autor da biblioteca codificou o prelúdio de Chopin, verificou-se que em várias ocasiões o compositor não seguiu as regras tradicionais:

O trabalho foi transcrito quase inteiramente, mas às vezes era necessário pular algumas notas, porque criavam os intervalos proibidos que Mezzo apontava.

Você pode perguntar quem se comprometeu a proibi-lo? Se Chopin não tem permissão para falar sobre o que é permitido na música ocidental e o que não é, então quem é?

O problema é que, embora o Mezzo possa levar em consideração o contexto, a estimativa de tipo continua sendo uma tarefa de escolha binária. Todas as notas estão corretas e o trabalho é compilado, se uma das notas está nocauteada e o trabalho não é compilado. E, apesar do Mezzo permitir que você escolha regras de composição, a decisão de aplicar ou não a regra é global. Se você desativar a regra porque alguma decisão musical viola o acordo usual, você cancelará a verificação de outras partes do trabalho.

Entropia digitada


Uma maneira de quebrar ou burlar as regras de digitação musical é modelar as transições entre as notas em termos de similaridade, seguindo os conselhos de Huron. Em vez de declarar uma transição específica certa ou errada, você pode calcular a quantidade de entropia que reflete a surpresa do público com as combinações de notas emparelhadas.

O código a seguir está escrito na linguagem funcional de tipo dependente Idris . No código, verifica-se que a melodia correspondente às regras começa com e termina com sal e que o caminho entre essas notas gera de 8 a 16 bits de entropia. Primeiro, você precisa determinar o tipo Melodyque reflete nossa representação da melodia com uma certa semelhança ou magnitude de entropia. Este tipo possui três construtores:

  • Pure: Reflete a criação de uma melodia a partir de uma única nota, com um nível de entropia superior e inferior igual a zero.
  • (>>=): pega duas melodias e adiciona seus limites de entropia com o custo de alternar de uma nota no final da primeira melodia para uma nota no final da segunda.
  • Relax: pega uma melodia e expande seus limites de entropia.

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)

Essa definição de tipo é mais complicada, mas graças a ela, Idris pode compor uma melodia usando notação do, e o compilador rastreará os limites da entropia para nós. Aqui está a melodia relevante com o baixo custo de todas as transições:

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

A música a seguir não está em conformidade com as regras, porque salta para um septo grande. No Mezzo, isso será proibido ou você precisará desativar completamente a regra. Aqui, apenas expandimos os limites da complexidade da melodia para que ela caiba no intervalo de 8 a 24 bits de entropia:

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

Se, em vez disso Melody (Do, So) (8, 24), atribuíssemos um tipo que não está em conformidade com as regras da melodia Melody (Do, So) (8, 16), ele não seria compilado!

A novidade da abordagem é que ela permite que você entenda quando a música se torna muito chata. Se a entropia da melodia não atingir o limite inferior, será gerado um erro de tipo. Portanto, se você atribuir um tipo a uma melodia que esteja em conformidade com as regras, Melody (Do, So) (16, 24)ela também não será compilada, porque sua entropia não atinge o limite inferior. Isso nos inspira a acreditar na teoria de Huron, segundo a qual será muito difícil para as pessoas ouvirem uma música que é muito incomum ou imprevisível.

No caso degenerado, as transições entre notas dentro da chave não aumentam a entropia e as transições fora da chave dão um aumento arbitrariamente grande na entropia. É aconselhável reverter para uma avaliação binária, na qual cada nota será considerada permitida ou proibida, sem status intermediário.

Importante, mas difícil de verificar


A verificação de tipos de música é difícil, porque é difícil determinar a correção da música. Se não podemos modelar matematicamente com precisão a definição de correção musical, não podemos transferi-la para o sistema de tipos. Mesmo que possamos formalizar autenticamente nosso entendimento, precisaremos fazer um esforço e aplicar um poderoso sistema de tipos para que o compilador possa avaliar adequadamente a melodia. No entanto, isso é possível com alguma definição e algumas suposições simplificadoras.

Isso é apenas curiosidade? Talvez. É improvável que a indústria da música adote em breve um sistema de tipos para evitar erros de composição. Mas se o estudo da computação no campo da música nos ajudar a avaliar diferentemente o que desempenha um papel tão importante na vida de quase todos nós, então isso por si só justifica todos os esforços.

Talvez não menos importante seja o fato de a música ser apenas uma das áreas em que a correção é importante, mas difícil de verificar. Quanto mais ativamente a esfera social e cultural é automatizada com a ajuda da programação, mais frequentemente surgem situações em que é difícil avaliar a resposta, que é crucial para as pessoas. Faça o uso de um programa de computador que decida quanto tempo a prisão . A correção das sentenças impostas depende de trocas complexas entre custos e probabilidades, e se não podemos rastrear a lógica da tomada de decisões pelo sistema, como podemos avaliar a justiça do resultado?

Sempre que automatizamos processos de tomada de decisão opacos, precisamos nos perguntar: "Como sabemos que o sistema está funcionando corretamente?"

All Articles