Re: C'est vrai que c'est plus verbeux en c++

Au temps pour moi, j'avais mal compris ce que tu voulais dire par là. Fréquentant peu le milieu des développeurs (que je lis surtout ici), je ne savais pas que les solutions orientées fonctionnelles étaient à la mode. De toute façon, les modes ça passe et ça repasse. ;-)

Cela étant, j'ai du mal à considérer les jugements disjonctifs et conjonctifs comme des notions sophistiquées. Ce qu'il y a, c'est qu'en POO la disjonction est abordée par la subdvision des concepts : l'héritage est un processus de spécification d'un genre (comme dans la proposition « un animal est un chien ou un chat ou une girafe... ») qui, comme l'a rappelé Guillaum, est ouvert par essence (nul ne peut dire a priori, c'est-à-dire statiquement, jusqu'où peut s'arrêter la spécification). L'avantage de la subdvision par les ADT est de fournir une partition exhaustive du type à diviser, et donc de pouvoir vérifier statiquement que tous les cas sont traités lors de la manipulation d'une valeur d'un tel type.

Comme l'a également rappelé Guillaum, les unions du C sont proches des ADT. Ce qu'il y a peut être de nouveau pour certains développeurs, c'est le vocabulaire employé pour qualifier ce genre de types : types de données algébriques. C'est lié aux relations que la disjonction et la conjonction entretiennent entre elles, et la façon dont elles opèrent l'une sur l'autre. Dans un choix comme celui d'un menu : (entrée et plat ) ou (plat et dessert), c'est équivalent au choix : plat et (entrée ou dessert). Ce qui n'est rien d'autre que la règle de distributivité de la multiplication sur l'addition : plat * (entrée + dessert) = (plat * entrée) + (plat * dessert).

En revanche, sur ce point :

Oui alors les types dépendants c'est une logique qu'un gamin de 4 ans comprends tout à fait.

je crois que tu surestimes grandement les capacités des enfants de 4 ans. ;-)

D'après mon expérience, un enfant de cet âge comprend tout à fait la logique propositionnelle (conjonction, disjonction et implication), c'est à dire celle qui sert de fondement au système de type de Haskell ou OCaml, mais ne sait pas raisonner si on introduit les notions de sujets et prédicats. Usuellement, on a plutôt fixé l'âge de raison à 7 ans; et encore même à 7 ans ce n'en est que des balbutiements.

Dans l'actualité récente, l'idée d'introduire les notions de sujet et prédicat dans les leçons de grammaire à partir des classes de CM1 a fait couler beaucoup d'encre : L'introduction du prédicat va-t-elle vraiment appauvrir la grammaire française ?. L'article est intéressant à lire, même si la notion n'est pas encore très claire pour son auteur. Comme dans l'exemple qu'il donne au début :

Par exemple, dans «cette polémique est totalement absurde», «cette polémique» est le sujet ; «est totalement absurde» est le prédicat, c’est-à-dire la partie de la phrase qui dit ce que le sujet fait ou est.

Ici le sujet est bien « cette polémique », mais le prédicat est « totalement absurde ». L'auxiliaire « être » constitue ce que l'on appelle la copule du jugement, c'est-à-dire la forme, là où le sujet et le prédicat en sont la matière. Comme dans le jugement suivant :

let l = [1; 2; 3];;
val l : int list = [1; 2; 3]

Le sujet est l, le prédicat int list et la copule est signifiée par le : entre eux. Ce que l'on exprimerait en français par la proposition : « la valeur l est une liste d'entiers ».

En revanche, les types dépendants ou leur forme affaiblie que sont les GADT ressemblent plus à des systèmes de types que je qualifierais de sophistiqués. Comme dans l'exemple suivant avec des GADT pour encoder la taille d'une liste dans son type.

module Llist = struct
 type z = Z (* zéro *)
 type 'n s = S : 'n -> 'n s (* la fonction successeur *)
 type un = z s (* un est le successeur de zéro *)
 type deux = un s (* deux est le successeur de un *)
 type trois = deux s (* trois est le successeur de deux *)
 type ('a,'n) t =
 | [] : ('a, z) t
 | (::) : 'a * ('a, 'n) t -> ('a, 'n s) t
 let rec zipwith :
 type a b c n. (a -> b -> c) -> (a, n s) t -> (b, n s) t -> (c, n s) t =
 fun f l l' -> match l, l' with
 | x :: [], x' :: [] -> (f x x') :: []
 | x :: y :: l, x' :: y' :: l' ->
 (f x x') :: zipwith f (y :: l) (y' :: l')
end;;
module Llist : sig
 type z = Z 
 type 'n s = S : 'n -> 'n s 
 type ('a, 'n) t = [] : ('a, z) t | (::) : 'a * ('a, 'n) t -> ('a, 'n s) t 
 val zipwith : 
 ('a -> 'b -> 'c) -> ('a, 'n s) t -> ('b, 'n s) t -> ('c, 'n s) t 
end

Ici on a des listes chaînées encodées via un GADT avec deux paramètres de types : a qui exprime le type homogène des éléments de la liste et n qui exprime la longueur de la liste (on encode les entiers dans le système de types via une représentation unaire, ce qui convient bien aux listes). Ainsi la fonction zipwith prend une fonction à deux paramètres et deux listes de valeurs, puis renvoie la liste des valeurs prises par la fonction. Mais ici, grâce au GADT, on peut exprimer dans le type de zipwith que les deux listes doivent être non vide et de même longueur (paramètre de type n s), sous peine de déclencher une erreur de typage à la compilation et non une erreur à l'exécution.

open Llist;;
let l : (int, deux) t = 1 :: 2 :: []
and l1 : (int, deux) t = 2 :: 3 :: []
and l2 : (int, trois) t =1 :: 2 :: 3 :: [];;
zipwith (+) l l1;;
- : (int, un s) t = :: (3, :: (5, []))
(* erreur à la compilation avec l de longueur 2 et l2 de longueur 3 *)
zipwith (+) l l2;;
Error: This expression has type (int, trois) t
 but an expression was expected of type (int, un s) t
 Type trois = deux s is not compatible with type un s 
 Type deux = un s is not compatible with type un = z s
 Type un = z s is not compatible with type z

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.