Les types paramétrés par des valeurs

Beaucoup de langages fortement typés autorisent les types paramétrés par des types (souvent appelés types génériques).
Coq autorise en plus les types paramétrés par des valeurs.

Pourquoi paramétrer un type par des valeurs ?

Parce que certaines opérations sur ce type de données ne sont possibles que pour certaines valeurs.
Par exemple 1|2 2|3 3|4 est une chaîne de dominos autorisée.
Tandis que 2|1 2|3 4|3 est une chaîne de dominos interdite.
D'où l'idée intuitive : paramétrons le type domino par un entier à gauche et un entier à droite.

Inductive domino : nat -> nat -> Type

Ensuite on ajoute block le constructeur de base et chain le constructeur composite. 

Inductive domino : nat -> nat -> Type :=
  | block: forall m n, domino m n 
  | chain: forall m n p, domino m n -> domino n p -> domino m p.

À partir de là Coq est capable de garantir (statiquement, à la compilation) qu'à l'exécution aucune chaîne invalide de dominos ne sera produite.

Création de la chaîne 1|2 2|3 :

Coq < Eval compute in chain 1 2 3 (block 1 2) (block 2 3).
     = chain 1 2 3 (block 1 2) (block 2 3)
     : domino 1 3

Le résultat est bien un domino 1|3 DoubleAccentCirconflexe

Laissez un commentaire

7 Commentaires

  • Hypolite Petovan *
    #0

    Félicitations pour le premier article créé sur la V9 !

    Je n'ai pas bien compris où étaient les valeurs paramètres du coup. Si tu paramètres par un entier à gauche et un entier à droite, ne paramètres-tu par par type ?

  • SpiceGuid *
    #1

    Le mieux que je puisse faire pour t'expliquer c'est un message d'erreur de typage.

    Par exemple la tentative de création de la chaîne 2|1 2|3 :

    > Eval compute in chain 2 1 3 (block 2 1) (block 2 3).
>                                          ^^^^^^^^^
Error: The term "block 2 3" has type "domino 2 3"
 while it is expected to have type "domino 1 3".

    Se solde par un échec car le type domino 2 3 n'est pas le type attendu.

  • Hypolite Petovan *
    #2

    Pour le coup j'ai parfaitement compris. Autre chose : dans ta définition tu n'as pas limité le chiffrage des dominos, il pourrait y avoir n'importe quel entier. Est-ce qu'il y a un moyen de limiter la fourchette de valeurs entre 1 et 6 ?

  • SpiceGuid *
    #3

    Déjà avec nat on élimine les entiers négatifs.
    Si on souhaite restreindre davantage il y a au moins deux façons de le faire.
    Vu qu'on n'utilise pas d'opération sur les nat on peut créer un type énuméré qui va de 1 à 6 :

    Inductive dice : Type :=
  one | two | three | four | five | six.

    Le type domino devient alors :

    Inductive domino : dice -> dice -> Type

    (Il faut toujours 2 valeurs dice pour instancier le Type domino)
    La seconde façon de faire c'est d'inclure la contrainte dans le constructeur block :

    Inductive domino : nat -> nat -> Type :=
  | block: forall m n, 1<=m<=6 -> 1<=n<=6 -> domino m n
  | chain: forall m n p, domino m n -> domino n p -> domino m p.

    Avantage : On dispose toujours des opérations dans nat.
    Inconvénient : Créer un block devient plus laborieux car on doit prouver qu'on respecte les bornes. On va créer une petite fonction dice pour simplifier la ligne block. 

    | block: forall m n, (dice m n) -> domino m n

    Normalement on préfère la 1ière façon car elle ne génére pas de nouvelle obligation de preuve, les valeurs étant d'emblée restreintes par la définition du type.

  • SpiceGuid *
    #4

    L'arbre de Fibonacci

    Un autre Type paramétré par une valeur entière.

    Inductive fibonacci : nat -> Type :=
  | zero: fibonacci 0
  | one:  fibonacci 1
  | plus: forall n, fibonacci n -> fibonacci (n+1) -> fibonacci (n+2).
  • Hypolite Petovan *
    #5

    Tu aurais un exemple d'utilisation de ce type ?

  • SpiceGuid *
    #6

    C'est pas comme si c'était un exemple pratique ouf
    C'est la limite théorique d'un tas de Fibonacci quand le nombre d'éléments tend vers l'infini.
    Les exemples plus concrets il y en a plein, la plupart du temps il s'agit d'expliciter une borne dans le type du conteneur pour garantir l'accès indicé.
    C'est de cas de vector dans la bibliothèque standard :
    vector est paramétré par un type A et par une valeur de ℕ (la longueur de la liste). 

    Inductive vector (A:Type) : nat ->  Type :=
  | nil:  vector A 0
  | cons: forall n, A -> vector A n -> vector A (n+1).

Laissez un commentaire

Vous devez être connecté pour commenter sur le Refuge. Identifiez-vous maintenant ou inscrivez-vous !


Marre des pubs ? Inscrivez-vous !

Tags