🕝 👱🏿 🙋🏿 Examen du système de type pour vérifier l'exactitude de la musique 🚿 🥓 🆗

Aujourd'hui, on parle beaucoup de la présentation de la musique à l'aide de langages de programmation, car d'une part c'est une tâche intéressante pour les ingénieurs, et d'autre part cela fait partie de la description universelle de la musique.

À quoi cela ressemble-t-il? Pour de nombreux langages, des environnements de programmation musicale ont été créés. Les plus populaires sont TidalCycles pour Haskell et Sonic Pi pour Ruby sur le Raspberry Pi. Il existe également un outil utilisant la bibliothèque de compositeurs de Leipzig . Comme il est écrit en Clojure, il manque une vérification de type.

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

La durée et la hauteur des sons sont représentées sous forme d'entiers et de coefficients littéraux, ce qui n'est pas très pratique. En matière de transformation musicale, la programmation peut être d'une grande aide. Disons que dans l'exemple ci-dessus, la tonalité est réglée sur la tonalité de do majeur et le tempo est de 90 battements par minute.

Lorsque les programmeurs voient du code musical, ils demandent le plus souvent s'il est possible d'empêcher une fausse exécution en utilisant un système de type. Bonne question. Si la musique peut être représentée sous forme de code, les erreurs d'écriture peuvent-elles être considérées comme des erreurs de programmation? Et si oui, pourquoi ne pas améliorer le processus d'écriture de musique en utilisant les techniques que nous utilisons pour écrire des programmes?

En particulier, il existe une analogie évidente entre les erreurs que le système de type peut empêcher et les cas courants d'inexactitude musicale. Si votre langage de programmation est capable de vérifier si vous avez passé une chaîne à une fonction qui s'attend à obtenir un nombre, alors il peut vérifier que vous n'utilisez pas f-sharp dans un passage écrit en do majeur, dont la clé ne présente aucun signe d'altération.

Dans cet article, nous découvrirons ce qui rend la musique correcte et comment elle peut être représentée à l'aide d'un système de type.

Prescriptivisme

Les théoriciens se disputent depuis des siècles sur ce qui rend la musique juste. Le plus souvent, ils opèrent dans le cadre du prescriptivisme musical: évaluer la conformité de la musique à un ensemble de règles.

Vous pouvez décrire la méthodologie dominante pour la formation des règles:

Apprendre le canon
Définition des motifs
Les formuler comme un ensemble de règles

On peut alors affirmer que:

La musique qui ne respecte pas ces règles est incorrecte.

Par exemple, la règle de composition stipule qu'il n'est pas permis de faire un saut vers un grand septima de à à s dans la mélodie. Cette approche a conduit à de nombreuses découvertes précieuses. La musique classique a des schémas extrêmement intéressants, et une généralisation de nos observations comme un ensemble de règles aide à discuter du phénomène de la musique.

De plus, suivre les règles est utile lors de la maîtrise d'instruments de musique. C'est bien quand les professeurs corrigent des enfants qui pratiquent le violon en do majeur, mais s'égarent. Il existe des situations dans lesquelles il est utile de respecter les définitions de la musique correcte et incorrecte.

Cependant, cette approche présente deux inconvénients principaux.

Premièrement, les règles découlant de ce processus dépendent fortement de ce que le théoricien considère comme canon. Le biais de l'ensemble de données conduit au biais des conclusions, et la musique classique occidentale ne reflète pas toute l'expérience musicale de l'humanité. Créer des règles basées sur la musique de Bach et de Mozart peut être amusant, mais elles ne vous en diront pas trop sur la musique en général.

La situation est compliquée lorsque vous réalisez que les genres musicaux sont souvent fortement associés à certaines cultures et groupes ethniques, et que donner la priorité à certains types de musique vous donne ainsi la priorité à votre insu à certains types de personnes. Par exemple, dans la théorie académique de la musique, une grande attention est accordée à l'étude des traditions européennes classiques et relativement peu à la musique provenant des diasporas d'immigrants d'Afrique: blues, jazz, rock and roll et hip hop. Si nous évaluons l'exactitude de la musique à travers la théorie traditionnelle, cela peut conduire à une version culturologique du problème lorsque les algorithmes de reconnaissance faciale fonctionnent mieux avec les Caucasiens qu'avec les Négroïdes.

Le deuxième gros inconvénient de la création de règles en identifiant et en généralisant les schémas est que de cette manière, nous nous concentrerons toujours sur le passé. Et la musique excite le plus lorsqu'elle enfreint les règles. Avant que Jimmy Page n'utilise l'effet de distorsion , les ingénieurs considéraient que l'écrêtage du signal pendant l'amplification était un défaut. Et bien que les modèles révélés aident à comprendre la musique moderne, cependant, ils ne conviennent absolument pas à l'évaluation de la musique future.

Un bon système de type pour la musique devrait éviter les deux pièges décrits du prescriptivisme. Il ne doit pas être basé sur des critères inacceptables ou subjectifs pour une musique correcte. Dans le même temps, en essayant de rendre les états erronés non représentables , le système de type ne devrait pas interférer avec l'apparition de nouveaux états.

Descriptivisme

Une alternative au prescriptivisme est le descriptivisme. Si dans le premier cas les motifs musicaux sont considérés comme des règles contraignantes, alors dans le second ils sont considérés comme des motifs qui se forment au cours de la pratique. Une approche descriptive de l'étude des règles musicales ressemble à ceci:

Explorer le corps de la musique
Identifier les tendances
Nous les formulons sous forme de modèle

On peut justifier par:

La musique s'écartant du modèle est inhabituelle.

Pour ce faire, nous avons besoin d'un bon modèle de structures musicales qui peuvent décrire l'ordinaire ou l'insolite, plutôt que le bien ou le mal. David Huron, dans son livre Sweet Anticipation, propose une théorie descriptive qui peut être réduite à trois aspects clés:

La musique est notée grâce à une formation statistique
Vous êtes satisfait des prévisions correctes
La nouveauté ne vous ennuie pas

Dans notre exemple prescriptivistique précédent, sauter d'une note à C est considéré comme une erreur. Et selon la théorie de Huron, ce sera très inhabituel. Ceux qui ont beaucoup écouté de la musique occidentale découvriront que lorsqu'ils entendent une note, la note suivante sera le plus souvent une autre note, ou une note un cran plus haut ou plus bas dans le son. Sauter vers le B surprendra le public, et ils pourraient prendre cela négativement.

L'une des conséquences curieuses de la théorie de Huron est que l'écriture de musique n'est pas un exercice pour maximiser ou minimiser la fiction. La musique se situe à la frontière entre l'ordre et le chaos, et l'emplacement des auditeurs dépend de la capacité du musicien à équilibrer le choc de la nouveauté avec la satisfaction de recevoir l'attendu. Si vous voulez vraiment vérifier l'exactitude de la composition, vous devrez vous assurer qu'elle ne va pas trop loin des traditions acceptées, mais aussi qu'elle ne les observe pas trop strictement.

Voici les données d'une analyse statistique des tendances mélodiques. Des couleurs plus foncées indiquent des résultats plus probables. Sélectionnez une ligne avec l'une des notes et trouvez-y une cellule avec une note qui est plus susceptible de suivre votre choix - l'intersection surlignée en noir avec la colonne d'une autre note. Par exemple, dans cet ensemble de données dans 33,53% des cas après la note, la note revient.

Ces données sont extraites du livre de Huron, elles sont le résultat de l'analyse de plus de 250 000 paires de sons de chansons folkloriques germaniques en majeur. Un autre ensemble de données, dites hip-hop ou rock and roll, démontrera différentes probabilités.

Toutes ces probabilités peuvent être représentées de manière équivalente sous forme de bits d'entropie: une probabilité de 50% correspond à un bit, une probabilité de 25% à deux bits, etc. Pour éviter de diviser par zéro, nous supposons que pour les transitions qui ne se produisent jamais dans l'ensemble de données, la probabilité est de 1/100 000. Maintenant, la couleur plus foncée montre des transitions plus coûteuses en termes d'entropie - c'est-à-dire moins probables. Par exemple, pour re après est égal à 6 bits d'entropie, c'est-à-dire qu'il a une probabilité de 1/64.

La représentation sous forme d'entropie nous aide à combiner la surprise d'une série de notes où chaque transition d'un son à un autre est un compteur d'entropie, la surprise de la mélodie entière étant la somme des transitions.

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

Ceci est très similaire au modèle de Markov caché , mais au lieu de générer des chaînes de notes, nous utilisons des probabilités pondérées pour estimer la probabilité d'une mélodie.

Vous avez peut-être remarqué que la transition de la note au do n'est que de 2,48 bits, bien qu'à première vue cela contredit le fait que la transition du do au do a été décrite ci-dessus comme très inhabituelle. Le plus souvent, les transitions inhabituelles représentent environ 10 bits d'entropie. La raison de cet écart est que les données huronnes ne font pas de distinction entre un saut de six notes de à à si (très inhabituel) et une transition d'une note de à à un si inférieur (une situation assez courante). Si les données nous permettent de séparer ces deux cas, le modèle montrera que la chaîne de do-si-mi-fa semblera encore plus non conventionnelle qu'avant-re-mi-fa.

Notes dactylographiées

Idéalement, un système de type aide les programmeurs à prendre les bonnes décisions et élimine la possibilité d'erreurs. Une bonne analogie musicale est le solfège. Si vous n'avez pas d'éducation musicale, vous pouvez vous familiariser avec le solfège sur la chanson Do-Re-Mi de la comédie musicale The Sound of Music . Chaque note d'une octave a son propre nom, et toute note en dehors de la tonalité du nom n'a pas:

À (note la plus basse de cet ensemble)
Ré
Mi
F
Sel
La
Si
À (maintenant une octave plus haut)

Ce système permet aux musiciens d'adhérer aux bonnes notes, il définit un mini-langage qui interdit de jouer des notes en dehors de la touche sélectionnée. Il existe une infinité de fréquences entre d et re, mais elles ne sont pas reproduites dans le solfège.

Cela peut être facilement représenté dans le code sous forme de données de type algébrique:

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

Vous pouvez maintenant définir des fonctions musicales qui n'autorisent pas les notes en dehors des touches. Par exemple, cette fonction répète une note n fois:

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

Avec cette définition, la triple répétition d'une note est une expression qui sera facilement comprise dans le domaine musical. Une répétition triple d'une forte netteté est une erreur de vérification de type, car la forte netteté n'est pas une valeur de type Solfege.

Cela nous donne un certain type de sécurité. Notre système nous permet d'éviter les mauvaises notes, mais il ne protège toujours pas contre les combinaisons incorrectes de notes. Si nous jouions en do majeur, nous ne jouerions pas en fa dièse, mais nous pourrions jouer en do, puis sauter à une grande septima sur une note en b, ce qui est interdit par les règles de composition (traditionnelles). Une telle vérification de type contextuelle est possible, mais nécessite une approche plus complexe.

Transitions typées

La bibliothèque Mezzo Haskell utilise des types connexes pour vérifier l'exactitude musicale. La description indique qu'il s'agit d'un "test très strict pour la musique", la bibliothèque peut vérifier la conformité aux différentes règles de composition, et pas seulement la tonalité. Dans Mezzo, le code suivant est compilé car la mélodie pré-re-mi-fa se compose des intervalles autorisés:

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

Mais si nous brisons la règle interdisant de sauter de à à si, alors Mezzo ne compilera pas un tel code:

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

C'est formidable que Mezzo signale même un problème:

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

Il peut sembler que le rêve de présenter une musique incorrecte comme des erreurs de type s'est réalisé. Mais des situations parfois délicates surviennent. Lorsque l'auteur de la bibliothèque a encodé le prélude de Chopin, il s'est avéré qu'à plusieurs reprises le compositeur n'a pas suivi les règles traditionnelles:

L'œuvre a été transcrite presque entièrement, mais il a parfois été nécessaire de sauter quelques notes, car elles créaient les intervalles interdits que Mezzo désignait.

Vous pouvez demander, qui s'est engagé à l'interdire? Si Chopin n'est pas autorisé à parler de ce qui est permis dans la musique occidentale et de ce qui ne l'est pas, alors qui alors?

Le problème est que même si Mezzo est capable de prendre en compte le contexte, l'estimation de type reste une tâche de choix binaire. Soit toutes les notes sont correctes et le travail est compilé, que l'une des notes soit supprimée ou que le travail ne soit pas compilé. Et malgré le fait que Mezzo vous permette de choisir des règles de composition, la décision d'appliquer ou de ne pas appliquer la règle est globale. Si vous désactivez la règle parce qu'une décision musicale viole l'accord habituel, vous annulerez la vérification des autres parties de l'œuvre.

Entropie typée

Une façon de briser ou de contourner les règles de frappe musicale est de modéliser les transitions entre les notes en termes de similitude sur les conseils de Huron. Au lieu de déclarer une transition particulière bonne ou mauvaise, vous pouvez calculer la quantité d'entropie qui reflète la surprise du public face aux combinaisons de notes.

Le code suivant est écrit dans le langage fonctionnel typé dépendant Idris . Dans le code, on vérifie que la mélodie correspondant aux règles commence par to et se termine par salt et que le chemin entre ces notes génère 8-16 bits d'entropie. Vous devez d'abord déterminer le type Melodyqui reflète notre représentation de la mélodie avec une certaine similitude ou ampleur d'entropie. Ce type a trois constructeurs:

Pure: Reflète la création d'une mélodie à partir d'une seule note, avec un niveau d'entropie supérieur et inférieur égal à zéro.
(>>=): prend deux mélodies et additionne leurs limites d'entropie avec le coût du passage d'une note à la fin de la première mélodie à une note à la fin de la seconde.
Relax: prend une mélodie et élargit ses frontières d'entropie.

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)

Cette définition de type est plus compliquée, mais grâce à elle, Idris peut composer une mélodie en utilisant la notation do, et le compilateur suivra les limites de l'entropie pour nous. Voici le morceau pertinent avec le faible coût de toutes les transitions:

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

L'air suivant n'est pas conforme aux règles, car il saute à un grand septima. Dans Mezzo, ce sera soit interdit, soit vous devrez désactiver complètement la règle. Ici, nous venons d'élargir les limites de la complexité de la mélodie afin qu'elle s'adapte à la plage d'entropie de 8 à 24 bits:

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

Si à la place Melody (Do, So) (8, 24)nous assignions un type non conforme aux règles de la mélodie Melody (Do, So) (8, 16), alors il ne compilerait pas!

La nouveauté de l'approche est qu'elle permet de comprendre quand la musique devient trop ennuyeuse. Si l'entropie de la mélodie n'atteint pas la limite inférieure, une erreur de type est générée. Donc, si vous affectez un type à une mélodie conforme aux règles, Melody (Do, So) (16, 24)elle ne sera pas non plus compilée, car son entropie n'atteint pas la limite inférieure. Cela nous inspire une foi dans la théorie huronne, selon laquelle il sera trop difficile pour les gens d'écouter de la musique trop inhabituelle ou imprévisible.

Dans le cas dégénéré, les transitions entre les notes à l'intérieur de la clé n'augmentent pas l'entropie et les transitions à l'extérieur de la clé donnent une augmentation arbitraire importante de l'entropie. Ensuite, il est conseillé de revenir à une évaluation binaire, dans laquelle chaque note sera considérée comme autorisée ou interdite, sans statut intermédiaire.

Important mais difficile à vérifier

La vérification des types de musique est difficile car il est difficile de déterminer l'exactitude de la musique. Si nous ne pouvons pas modéliser mathématiquement avec précision la définition de l'exactitude musicale, nous ne pouvons pas la transférer dans le système de types. Même si nous pouvons formaliser authentiquement notre compréhension, nous devrons faire un effort et appliquer un système de type puissant afin que le compilateur puisse évaluer correctement la mélodie. Cependant, cela est possible avec une certaine définition et quelques hypothèses simplificatrices.

Est-ce juste de la curiosité? Peut être. Il est peu probable que l'industrie de la musique adopte bientôt un système de type pour éviter les erreurs de composition. Mais si l'étude de l'informatique dans le domaine de la musique nous aidera à évaluer différemment ce qui joue un rôle si important dans la vie de presque tous, alors cela seul justifie tous les efforts.

Peut-être pas moins important est le fait que la musique n'est qu'un des domaines où l'exactitude est importante, mais difficile à vérifier. Plus la sphère sociale et culturelle est automatisée à l'aide de la programmation, plus il se produit souvent des situations dans lesquelles il est difficile d'évaluer la réponse, ce qui est crucial pour les gens. Prenez l' utilisation d'un programme informatique qui décide de la durée de l'emprisonnement . La justesse des peines infligées dépend de compromis complexes entre les coûts et les probabilités, et si nous ne pouvons pas suivre la logique de la prise de décision par le système, comment pouvons-nous évaluer l'équité du résultat?

Chaque fois que nous automatisons des processus de décision opaques, nous devons nous demander: "Comment savons-nous que le système fonctionne correctement?"