Je ne vois toujours pas en quoi ils n'ont pas de type au sens IT du terme.
Il n'existe pas d'opération typeof qui retourne le type de l'objet, car il existe une infinité de collection distincte qui contiennent cet objet.
Je crois que ce que kantien tente de te dire, c'est qu'en restant sur l'aspect purement mathématique (vu que le sujet t'intéresse), ce que tu appelles « collection » forme un type ou « ensemble de valeurs »
L'opposition « type au sens IT » ne fait pas sens pour tout le monde... parce-que d'une part IT est un peu vague et surtout d'autre part ne recouvre pas les expériences de tout le monde. Or kantien a une autre expérience des langages (à la lecture il ne fait pas que du OCaml mais aussi fort vraisemblablement des langages de preuve et de spécification formelle ?) bien différente de la tienne.
Un type c'est un ensemble de valeurs (comme N, Q ou R)
Ce qui n'est pas le cas dans la plupart des langages de programmation, en C, en C++, en Python, en Java, etc... le type est une propriété intrinsèque de la-dite valeur.
Voilà, le type en C n'est pas le type en OCaml ni le type en Prolog ni le type en Lisp ni...
Pour des langages comme C/C++/Python/Java la notion de type est plutôt loin de la définition mathématique des ensembles (malgré le parallèle en surface) car ce qui est appelé type est plutôt pour la représentation en mémoire... Un langage pour lequel on doit se préoccuper de savoir comment on interprète chaque octet (int/byte/float/char/whatever) a un typeof alors que d'autres langages s'en foutent (ou du moins c'est transparent pour les usagers.)
Dans ton exemple, OCaml croit que l'on ne peut pas additionner des nombres pairs, ce qui est complètement faux.
C'est juste que l'exemple choisi fait lever une alerte (ce n'est pas une erreur ou une impossibilité) sur une ambiguïté : doit-on considère qu'on reste en nombres pairs (et donc si pour une raison quelconque on se retrouve avec des trucs impaires ça passe pas) ou doit-on juste voir que ce sont des entiers après tout (et donc il n'y a pas de problème si on se retrouve avec des impaires.) Ce genre de comportement n'est pas lié aux typeof stricto-sensus mais au fait que ces langages se veulent un peu contraint (c'est le cas aussi en Ada, parce-que tu peux avoir défini un ensemble comme des pointures de chaussure et l'autre comme des nombres de paire de chaussures, donc on peut additionner mais le compilo craint d'additionner des choux et des carottes là où justement C n'y aurait vu que du feu.)
"It is seldom that liberty of any kind is lost all at once." ― David Hume
[^] # Re: théorie des ensembles pas naives
Posté par Gil Cot ✔ (site web personnel, Mastodon) . En réponse au journal [Letlang] Et si on rédigeait la spec ?. Évalué à 7.
Je crois que ce que kantien tente de te dire, c'est qu'en restant sur l'aspect purement mathématique (vu que le sujet t'intéresse), ce que tu appelles « collection » forme un type ou « ensemble de valeurs »
L'opposition « type au sens IT » ne fait pas sens pour tout le monde... parce-que d'une part IT est un peu vague et surtout d'autre part ne recouvre pas les expériences de tout le monde. Or kantien a une autre expérience des langages (à la lecture il ne fait pas que du OCaml mais aussi fort vraisemblablement des langages de preuve et de spécification formelle ?) bien différente de la tienne.
Voilà, le type en C n'est pas le type en OCaml ni le type en Prolog ni le type en Lisp ni...
Pour des langages comme C/C++/Python/Java la notion de type est plutôt loin de la définition mathématique des ensembles (malgré le parallèle en surface) car ce qui est appelé type est plutôt pour la représentation en mémoire... Un langage pour lequel on doit se préoccuper de savoir comment on interprète chaque octet (int/byte/float/char/whatever) a un
typeofalors que d'autres langages s'en foutent (ou du moins c'est transparent pour les usagers.)C'est juste que l'exemple choisi fait lever une alerte (ce n'est pas une erreur ou une impossibilité) sur une ambiguïté : doit-on considère qu'on reste en nombres pairs (et donc si pour une raison quelconque on se retrouve avec des trucs impaires ça passe pas) ou doit-on juste voir que ce sont des entiers après tout (et donc il n'y a pas de problème si on se retrouve avec des impaires.) Ce genre de comportement n'est pas lié aux typeof stricto-sensus mais au fait que ces langages se veulent un peu contraint (c'est le cas aussi en Ada, parce-que tu peux avoir défini un ensemble comme des pointures de chaussure et l'autre comme des nombres de paire de chaussures, donc on peut additionner mais le compilo craint d'additionner des choux et des carottes là où justement C n'y aurait vu que du feu.)
"It is seldom that liberty of any kind is lost all at once." ― David Hume