Version imprimable
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.
Faire des entiers type-level, c'est facile :
Code:
2
3
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é...
Citation:
Envoyé par prgasp77
en suivant l'idée de bluestorm, as-tu vu ceci : http://till-varoquaux.blogspot.com/2...tom-types.html ?Citation:
Envoyé par bluestorm
la beauté des types phantom :)
+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"Citation:
Envoyé par bluestorm
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.Citation:
Envoyé par prgasp77
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.
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.
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.mlCode:
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
34module 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:
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
35module 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.
Citation:
Envoyé par prgasp77
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 :)