Discussion :

[prgasp77]

Bonjour à tous,
je cherche à créer un type représentant un 'a vector tel que deux vecteurs de dimensions différentes soient de type différent. J'ai fait quelques recherches et suis tombé sur cet article qui traite du problème en Haskel.

Je n'ai pas réussi à transcrire la solution à Caml . Je demande donc un petit coup de pouce. Merci.

[gasche]

Faire des entiers type-level, c'est facile :

Code ocaml :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
 
type zero
type 'a succ

Ce qui est difficile c'est de supporter les opérations qui t'intéressent. Tu ne peux pas espérer par exemple forcer le compilateur à inférer le bon type à la création du tableau, il faut le fournir (et il ne sera sans doute même pas capable de vérifier qu'il concorde avec la longueur donnée). Pour le reste, tu peux avoir du typage, mais si tu veux la concaténation de tableaux par exemple il faut l'addition des entiers-types, ce qui est plus difficile.

Haskell est mieux doté que OCaml grâce aux GADTs (mais il existe une extension OCaml pour les GADT, si ça t'intéresse), qui permettent de formaliser des contraintes d'égalité entre types, aux types-classes qui permettent de faire un peu de programmation logique au niveau des types (mais très laid et ad-hoc), et aux type-level functions quand, les bons jours, elles ne cassent pas la consistence du système de type.

On peut faire un peu mieux avec OCaml 3.12, qui permet en substance d'encoder les GADTs avec les modules de première classe. Encore une fois c'est Oleg qui fait le plus de bruit là-dessus (mais ce n'est pas le seul à en parler et le faire) : http://okmij.org/ftp/ML/first-class-modules/

Tout ça, ça reste des encodages assez lourds et assez fragiles. Si tu veux vraiment délirer avec des types dans tous les sens, essaie un langage avec des types dépendants, comme Coq, Agda ou Epigram. Je ne garantis pas par contre que ça augmente ta productivité...

[gorgonite]

je cherche à créer un type représentant un 'a vector tel que deux vecteurs de dimensions différentes soient de type différent.

Faire des entiers type-level, c'est facile ...

en suivant l'idée de bluestorm, as-tu vu ceci : http://till-varoquaux.blogspot.com/2...tom-types.html ?
la beauté des types phantom

Tout ça, ça reste des encodages assez lourds et assez fragiles. Si tu veux vraiment délirer avec des types dans tous les sens, essaie un langage avec des types dépendants, comme Coq, Agda ou Epigram. Je ne garantis pas par contre que ça augmente ta productivité...

+1 avec bluestorm sur ce point... si tu as vraiment besoin de ce niveau de précision sur les types, mieux vaut t'orienter vers un langage qui gère réellement un système "aussi puissant"

[LLB]

je cherche à créer un type représentant un 'a vector tel que deux vecteurs de dimensions différentes soient de type différent.

Tu as un besoin réel en pratique ? Je sais que c'est amusant, mais c'est rarement utile en vrai. Il est rare de connaître la taille de tous ses tableaux et de pouvoir se limiter aux quelques fonctions implémentables.

Il m'est quelques fois arrivé de vouloir vérifier que deux tableaux constants ont la même taille (si j'en modifie un, je dois penser à modifier l'autre), mais ça se résout facilement : en C, je ferais un static_assert ; en Caml, un assert au début du programme est largement suffisant.

[prgasp77]

Bonjour et avant tout merci.

J'ai été étonné par la qualité des réponses, on ne trouve ça que dans le forum caml je crois . J'ai travaillé à partir des pistes lancées, tout cela semble prommetteur, mais je me heurte encore à quelques soucis, notamment pour "encapsuler" ce type dans un module. Je reviendrai plus tard sur mon problème une fois mes recherches personnelles terminées.

J'aimerais aussi m'excuser pour mon délai de réponse, alors que vous avez été si rapide à m'aiguiller. J'ai eu quelques semaines chargées, désolé.

Bonne continuation à tous sur dvp.

[prgasp77]

Bonjour,
j'ai finalement une très bonne base pour arriver à mes fins. En voici une ébauche didactique qui je l'espère servira à quelqu'un.

Vector.ml

Code OCaml :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
module type Korps =
  sig
    type t
    val zero: t
    val one: t
    val neg: t -> t
    val inv: t -> t
    val add: t -> t -> t
    val mul: t -> t -> t
  end

module type Vector =
  sig
    type scalar
    type ('a,'b) t
    type zero
    type 'b succ
    val nil: (scalar,zero) t
    val cons: scalar -> (scalar,'a)t -> (scalar,'a succ) t
    val to_list: ('a, 'length) t -> scalar list
    val add: ('a, 'length) t -> ('a, 'length) t -> ('a, 'length) t
  end

module Make(K:Korps) : (Vector with type scalar = K.t) =
  struct
    type scalar = K.t
    type zero
    type 'b succ
    type ('a, 'length) t = scalar list
    let nil = []
    let cons = fun hd tl -> hd::tl
    let to_list = fun l -> l
    let add = List.map2 K.add
  end

Usage

Code OCaml :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
module Z =
struct
  type t = int
  let zero = 0
  let one = 1
  let add = (+)
  let mul = ( * )
  let inv = (/) 1
  let neg = (~-)
  end
;;

module Zn = Vector.Make(Z)
;;
let v1 = Zn.cons (-1) (Zn.cons 5 Zn.nil)
;;
let v2 = Zn.cons 2 (Zn.cons 3 Zn.nil)
;;
let v3 = Zn.add v1 v2
;;
Zn.to_list v3
;;
- : Zn.scalar list = [1; 8]
Zn.add Zn.nil v1
;;
Characters 14-16:
  Zn.add Zn.nil v1 ;;
                ^^
Error: This expression has type
         (Zn.scalar, Zn.zero Zn.succ Zn.succ) Zn.t =
           (Zn.scalar, Zn.zero Zn.succ Zn.succ) Make(Z).t
       but an expression was expected of type
         (Zn.scalar, Zn.zero) Zn.t = (Zn.scalar, Zn.zero) Make(Z).t
       type Zn.zero Zn.succ Zn.succ = Zn.zero Zn.succ Make(Z).succ
       is not compatible with type Zn.zero = Make(Z).zero

On voit bien que l'interpréteur distingue bien les types des vecteurs de dimensions différentes. Je vous remercie à nouveau pour toute l'aide que vous m'avez apportée, rapidement et de manière très pertinente. Je me permets de clore mon sujet par une question a priori ouverte : y a-t-il un moyen pour que l'interpréteur affiche un message d'erreur plus compréhensible lorsque l'on utilise un sous-type vecteur pour un autre de dimension différente (cas de la dernière commande) ?


Je rappelle aussi que la plupart du code ci-dessus provient d'un article d'un blog proposé par gorgonite ; et que tout ceci n'est au final qu'une version orientée module du travail original.

[gorgonite]

Je me permets de clore mon sujet par une question a priori ouverte : y a-t-il un moyen pour que l'interpréteur affiche un message d'erreur plus compréhensible lorsque l'on utilise un sous-type vecteur pour un autre de dimension différente (cas de la dernière commande) ?

C++ a le même problème avec ses erreurs sur les templates... il faut savoir traduire, car on joue avec une construction qui dépasse (un peu) le système de type "natif" et donc le message n'est pas aussi explicite