Library FingerTree.DependentFingerTree

On va maintenant définir la structure de sur un monoïde et une mesure donnée. On verra dans la section comment diverses instantiations de ces paramètres permettent de dériver différentes structures.

La variable v représente le support du monoïde et mono est l'implémentation du monoide elle-même. Bien sûr, on a toujours accès au notations ε et ∙ pour se référer aux méthodes de la classe Monoid.

Nodes

On a déjà défini les doigts, on définit maintenant les nœuds 2-3 paramétrés par une mesure. Les node cachent aussi une mesure qui contient la combinaison des mesures des sous-objets.

On dénote encore une fois la fonction measure par dans la suite.

On utilise un type sous-ensemble ici pour spécifier l'invariant sur la valeur cachée. Cet invariant ne peut pas être vérifié à l'aide de types simples puisqu'il dépend évidemment des valeurs portées par le constructeur de node. De plus, l'invariant fait référence à la de mesure, qui va donc devenir un du type de donnée, ce qui requiert un mécanisme d'abstraction supplémentaire dans les langages fonctionnels courants, comme les classes de type de ou un système de module avec foncteurs à la . Ici, on utilise simplement le produit dépendant.

On peut aussi définir les node2 et node3 qui calculent les mesures à la volée. On caste les expressions avec le type v pour désambiguer la surcharge qui sinon chercherait une instance de Monoid sur le type sous-ensemble {s : v | s = lparr x rparr ∙ lparr y rparr }.

Les obligations générées sont trivialement vraies, elles sont de la forme . De façon correspondante, node_measure projette la mesure cachée. On a ici une projection implicite.

On peut déclarer une instance globale (généralisée à la sortie de la section) pour la mesure d'un nœud.

On peut toujours convertir un node en digit en oubliant la mesure.

Bien qu'il puisse sembler que la fonction node_measure est indépendante de la fonction measure, elle ne l'est pas. En effet le type de cette fonction après la clôture de la section devient: Π (m : Monoid v) (A : Type) (ms : Measured A), node → v

L'inductif node lui-même est paramétré par la fonction de mesure, donc toutes les opérations sur les nœuds la prennent comme argument implicite (à la manière d'une contrainte de classe sur un type de donnée en ). On a donc gratuitement la propriété qu'on ne peut pas confondre deux objets de type node construits avec des mesures différentes sur le même type d'éléments puisque la mesure fait partie du type.

Si nous n'avions pas ajouté l'invariant au sein des constructeurs, nous n'aurions pas besoin de ce paramètre, mais nous ne pourrions pas prouver grand chose sur les mesures qui seraient des objets arbitraires de type v. On pourrait définir un prédicat inductif sur les node assurant que la mesure d'un nœud a bien été construite en utilisant la mesure de façon cohérente, mais on aurait à montrer la préservation de ce prédicat pour toutes les fonctions manipulant directement ou indirectement des nœuds. Ici, on garantit cette propriété par le typage et le système nous donnera automatiquement les obligations à montrer lorsque l'invariant pourrait être cassé.

Finger Trees

Avant de présenter la définition de fingertree en , on rappelle le type original et on va justifier pourquoi une traduction directe serait insatisfaisante. Le type des mesurés est défini comme suit:



La figure représente un exemple de mesuré.



On pourrait directement définir la structure de en en traduisant la définition . Seulement, en faisant cela on pourrait causer un certain nombre de difficultés. Premièrement, on aurait le même problème décrit auparavant d'identification de structures qui ont été construites par des mesures différentes si l'on ne paramétrait pas le type par celle-ci. Bien sûr, le fait de paramétrer par la mesure force à réinstancier celle-ci au nœud Deep puisque le sous-jacent attend une mesure sur des objets de type plutôt que α.

Un est donc paramétré par un type A et une fonction de mesure sur ce type. Chaque objet de type fingertree est aussi indexé par sa propre mesure:

• Empty construit l'arbre vide de mesure ε;
• Single x construit l'arbre singleton de mesure ;
• Deep pr ms m sf construit un arbre de préfixe pr, sous-arbre m de mesure ms et suffixe sf. Sa mesure est calculée en combinant les mesures de ses sous-structures de gauche à droite. L'argument ms sera implicite lorsqu'on construira des nœuds Deep puisqu'on peut l'inférer à partir du type de m. On place cette mesure cachée juste avant l'arbre du milieu contrairement à la version originale où la mesure est le premier composant et stocke la mesure de l' de l'arbre. Pour nous, la mesure de l'arbre complet est donnée par l'index. On présente la définition sous forme de règles d'inférence pour une meilleure lisibilité, en omettant les paramètres A et measure dans les prémisses:

Cette famille inductive est indexée par des valeurs de type v. Une simple observation nous a conduit à ce type dépendant: nous voulons avoir l'invariant que la mesure cachée sur le nœud Deep est bien celle du sous-arbre. Pour cela on doit avoir une façon de référer à cette mesure au moment même de la définition de l'arbre, alors qu'on ne peut pas écrire une fonction récursive (polymorphe) sur l'arbre, à moins de se placer dans le cadre des définitions inductives-récursives . La mesure de l'arbre fait ici partie de son type. On va donc faire apparaître les invariants sur les mesures contenues dans nos arbres directement dans les types des fonctions sur les fingertree.

Ajouter un élément

On peut ajouter un élément a à gauche d'un arbre t de mesure s pour obtenir un arbre de mesure measure a ∙ s. Du fait de la récursion polymorphe, toutes nos fonctions récursives vont maintenant avoir des arguments A et measure puisqu'ils sont de arguments qui changent lors des appels récursifs. Si t est vide, un singleton ou un arbre avec un préfixe gauche non plein, on pousse simplement a à la position la plus à gauche de l'arbre. Sinon, on doit réorganiser l'arbre pour faire de l'espace à gauche pour a. Cela requiert une récursion polymorphe pour ajouter un élément node3 measure c d e à gauche de t' : fingertree v (node_measure measure) st'.

La première expression match utilise l'élimination dépendante. Le sens des annotations est qu'à partir d'un fingertree d'une mesure s particulière, chaque branche doit construire un fingertree de mesure measure a ∙ s ou s sera substitué par la mesure correspondant au motif de la branche. Par example, dans la première branche on doit construire un objet de type fingertree measure (measure a ∙ ε). Seulement, la branche droite Single a a le type fingertree measure (measure a), on utilise donc la règle d'équivalence sur les familles inductives présentée figure pour coercer l'objet dans le type attendu. L'application de cette règle génère une obligation , facilement résolue en utilisant la loi d'identité à droite du monoïde. Les clauses in et return sont en général obligatoires en à cause de l'indécidabilité de l'unification d'ordre-supérieur (il faudrait trouver le type le plus général unifiant les types des branches, en inférant les dépendances avec l'objet filtré). On peut cependant les omettre dans , auquel cas la substitution utilisée par l'élimination dépendante est remplacée par du raisonnement équationnel. Si nous avions omis ces clauses, on aurait eu l'équation s = ε dans le contexte de la première branche et donc l'obligation . Celle-ci serait résolue par substitution de s par ε dans le but puis application de l'identité à droite ; on a juste retardé la substitution.

Le filtrage imbriqué sur le préfixe de l'arbre utilise un x pour capturer les préfixes qui ne sont pas Four et applique la fonction "partielle" add_digit_left définie précédemment. On a une application de la règle d'équivalence sur les sous-ensembles ici, qui génère une obligation de montrer que x n'est pas plein. Celle ci peut être résolue parce que l'algorithme de compilation du filtrage ajoute une hypothèse dans le contexte. On enrichit les contextes de typage des branches par ce genre d'inégalités lorsque leurs motifs sont en intersection avec des motifs précédents.

La préservation de la mesure est une propriété essentielle de cette fonction. Pour le voir, prenons l'instantiation des par le monoïde des listes avec la concaténation. On peut vérifier ici qu'ajouter un élément à gauche de l'arbre insère bien la mesure de l'élément devant la mesure de l'arbre. Cela revient donc à ajouter un élément en tête de la liste des éléments de l'arbre original avec ce monoïde des listes. Pour chacune des définitions suivantes, cette correspondance avec l'interprétation des listes aura toujours un sens évident. On définit la fonction de la même façon.

Un exemple plus simple d'élimination dépendante nous est donné par la fonction de conversion digit_to_tree, qui transforme un "doigt" en un arbre de même mesure. Notons qu'ici on omet les annotations. Les versions récentes de sont capables dans le cas où l'on filtre une variable qui apparaît dans le type de retour d'inférer automatiquement le prédicat d'élimination dépendante. On utilise aussi cette optimisation dans , qui permet d'utiliser la substitution le plus possible mais toujours en conservant les équations dans chaque branche.

La vue à gauche d'un

On va maintenant construire des vues sur les qui permettent de décomposer un arbre en son premier élément (à gauche ou à droite) puis le reste de l'arbre. Cela permet de s'abstraire de l'implémentation et donner une interface similaire aux listes au type de donnée fingertree. On peut ainsi écrire des fonctions récursives sur les sans avoir à s'occuper des détails compliqués de la structure (voir par exemple la définition de merge).

Le type inductif de la vue à gauche View_L est un peu moins polymorphe que les autres, puisqu'il n'a pas besoin de contenir la fonction de mesure que les vues ignorent. En revanche on stocke la mesure s du reste de l'arbre dans le constructeur cons_L (s sera implicite). On abstrait donc View_L par le type de la séquence seq indexé par un objet de type v. On l'instanciera par fingertree A.

Une telle vue sera produite par la fonction view_L, par récursion structurelle (polymorphe) sur le fingertree. On peut facilement utiliser la fonction partielle digit_tail qui n'accepte que les digit non-singleton et l'on n'a besoin d'aucune annotation de type à l'appel récursif de view_L. Notons qu'on utilise une de type (fingertree A) dans le type de retour, ce qui est parfaitement légal en .

On peut montrer que view_L préserve la mesure de l'arbre. Si nous avions indexé View_L par la mesure de l'arbre en entrée, ces lemmes de génération seraient apparus comme obligations dans la définition de view_L.

Problèmes de dépendance

Nos vues sont utiles pour construire une interface de haut-niveau sur les , mais dans leur état courant elles sont très limitées puisqu'on ne peut écrire que des fonctions non-récursives sur ces vues. En effet, on ne peut pas convaincre qu'une fonction définie par récursion sur la vue d'un arbre est aussi valide que par récursion sur l'arbre lui-même, à cause de la condition de garde. Pour ce faire, nous avons besoin d'une mesure sur le type fingertree, par exemple leur nombre d'éléments donné par la fonction tree_size. On peut dès lors créer une mesure trivialement sur les vues View_L_size. Les définitions de tree_size et donc View_L_size sont généralisées pour toute fonction de taille à cause de la récursion polymorphe.

Il n'y a plus qu'à montrer que pour tout arbre t, view_L t retourne une vue de taille tree_size t pour prouver qu'un appel récursif sur la queue d'une vue est correct (c.f. ).

Seulement, faire cette preuve n'est pas si facile parce que view_L manipule des objets à type dépendant et raisonner sur ceux-ci est assez délicat. Une difficulté essentielle est que l'égalité de Leibniz n'est pas adaptée pour comparer des objets dans des types dépendants puisqu'ils peuvent être comparables mais dans des types différents. Par exemple la proposition sur les vecteurs vnil = vcons x n v n'est pas bien typée puisque vnil est de type vector 0 et vcons x n v de type vector (S n). Ces deux types n'étant pas convertibles, on ne peut même pas typer cet énoncé.

Dans notre cas, on veut montrer qu'un arbre t arbitraire de mesure s ayant pour vue nil_L est forcément l'arbre vide Empty, mais ces deux termes n'ont pas le même type. On applique la solution proposée par en utilisant une égalité hétérogène: on va alors pouvoir prouver que les termes doivent être dans le même type et retrouver l'égalité de Leibniz ensuite. L'inductif JMeq definit l'égalité hétérogène (denotée par ) en , de type: ∀ A (a : A) B (b : B), Type. Cette égalité permet de comparer des objets qui ne sont pas du même type (ou pas encore, avant simplifications dues à des réécritures, des éliminations). Son unique constructeur est JMeq_refl, de type Π A a, JMeq A a A a. L'intérêt de cette notion d'égalité est de retarder le moment où l'on doit montrer que deux types sont égaux et donc que deux objets sont comparables. Lorsqu'on arrive à raffiner une hypothèse d'égalité dépendante pour que les deux types coincident, on peut appliquer l'axiome JMeq_eq de type Π A x y, JMeq A x A y → x = y pour récupérer une égalité de Leibniz usuelle entre les deux objets. L'axiome JMeq_eq est équivalent à l'axiome de .

Dans le premier lemme, on compare t de mesure s avec Empty de mesure ε; clairement, si l'on remplace JMeq par l'égalité de Leibniz on aura une erreur de typage.

Une fois qu'on a montré l'égalité pour un index général s, on peut l'instancier sur un index particulier, ici ε. Sachant que t est maintenant de mesure ε, on peut utiliser l'égalité de Leibniz entre t et Empty.

Ces lemmes auxiliaires sur nil_L et Empty vont nous permettre de construire la mesure. En effet, ils sont nécessaires pour prouver le lemme suivant:

Cela nous donne une mesure décroissante sur les résultats de view_L. On l'utilisera plus tard, lorsqu'on programmera des instances.

On peut aussi définir le deep_L, qui réarrange un arbre lorsqu'on lui donne un digit de préfixe potentiel et inversement pour deep_R. C'est une version dépendante de la fonction interne pour le cas Deep de view_L, qui est utilisée lorsqu'on découpe des . On peut noter que la spécification bénéficie de la surcharge qui permet de factoriser toutes les instances de measure sur les arbres, les doigts et les doigts optionnels dans ce cas.

De retour à la normale

À l'aide de ces vues, on peut maintenant implémenter facilement les opérations de sur le type fingertree. On n'a pas besoin de récursion ici, on peut donc définir ces opérations sur un type A, une mesure measure et un index s fixés dans une section.

On définit un prédicat isEmpty pour les fonctions définies seulement sur les arbres non vides. Cette fois-ci, on ne filtre pas directement sur l'objet mais sur la vue pour maintenir l'abstraction vis-à-vis de l'implémentation.

On peut évidemment décider si un arbre est vide ou non.

Les opérations évidentes sont définissables, on montre la fonction liat duale de tail. Ici on retourne une mesure accompagnée d'un fingertree dans une paire dépendante de type {s : v & fingertree A s}, qui correspond bien à la vue de la mesure comme une donnée et pas seulement un indice qui raffine le type de données. On note la construction d'une telle paire d'un arbre t avec sa mesure m par m :| t, qui se lit "m mesure t".

Concaténation et découpage dépendants.

On peut aussi définir la concaténation avec un type dépendant exprimant clairement sa spécification. L'implémentation est la même que celle d'Hinze & Paterson, excepté qu'on a prouvé les 100 obligations générées par concernant les mesures. Les cinq fonctions mutuellement récursives cachées ici qui définissent app ont la particularité d'être assez longues (près de 200 lignes au complet) puisqu'elles implémentent une spécialisation de la concaténation comme nous l'avons décrit plus haut . On vérifie ici statiquement que la définition est correcte: le type indique qu'on a bien la propriété évidente sur les que la concaténation de deux arbres donne un arbre dont la mesure est la concaténation des mesures des deux arbres.

La dernière opération, qui a certainement la plus intéressante spéficication du développement, est le découpage d'un arbre par un prédicat sur sa mesure. On commence par découper un nœud.

On découpe un nœud n par un prédicat p en cherchant où celui-ci s'évalue à true, en commencant par la mesure initiale i et en accumulant les mesures des sous-objets de gauche à droite. On a simplement copié l'invariant donné dans sans rien y changer. On a simplement ajouté une propriété sur les mesures qui généralise l'équation sur to_list. Le code est aussi une traduction directe du code en , on utilise juste un produit cartésien au lieu d'un nouveau type inductif split. On a aussi défini une opération split_digit avec une spécification similaire.

Le cas le plus intéressant est celui des arbres. Plutôt que de retourner un tuple raffiné dans un type sous-ensemble, on définit cette fois une famille inductive tree_split qui capture l'invariant qu'un découpage est une décomposition d'un fingertree préservant sa mesure. On ajoute aussi les invariants sur les arbres de gauche et droite vis-à-vis du prédicat. Ils pourront être utilisés par les clients pour prouver des propriétés sur leur code. L'inductif tree_split est en fait une dépendante d'un arbre. C'est une particularité de la programmation avec types dépendants et de ce développement en particulier: on dérive non seulement du code réutilisable mais aussi des preuves réutilisables en utilisant des types riches. En effet, la fonction de découpage peut être vue comme un combinateur de preuves, relevant une propriété sur une mesure et un monoïde en une propriété sur les mots de ce monoïde représentés par les fingertree.

Ce type inductif combine des types sous-ensemble et dépendants, mais nous pouvons toujours écrire notre code comme d'habitude. Approximativement 100 lignes de preuves sont nécessaires pour décharger les obligations générées par cette définition.

Ceci conclut notre implémentation des dépendants avec . Pour résumer, nous avons prouvé que:

• Toutes les fonctions sont totales une fois annotées par leurs préconditions.
• Toutes les fonctions respectent la sémantique des mesures qui est rendue explicite dans les types alors qu'elle était auparavant implicite dans le code.
• Toutes les fonctions respectent les invariants donnés dans le papier original par Hinze & Paterson.