surtout pas très pertinent pour un système de types informatiques
En quoi c'est pas pertinent ? Je parle de l'inspiration derrière le système de type afin de présenter le système de type justement qui diffère de la plupart des autres langages de programmation.
Mais dire qu’il n’y a pas de "types" en mathématiques est toujours faux.
Il n'y a pas de "type" au sens informatique du terme. Le "type" au sens mathématique du terme c'est l'appartenance à une collection muni ou non d'opérations. Et un objet n'a pas un unique type car c'est la définition de la collection qui détermine cette appartenance.
Si tu dis ∀x ∈ Q tel que x = 42, ∀y ∈ R tel que y = 42 : en toute rigueur x ≠ y.
Mais en pratique c'est le cas. x et y désignent tout deux le même objet qui, par la définition de Q et R, appartient aux 2 ensembles.
Par abus les mathématiciens finissent par dire que x = y. Mais c’est pas si évident que ça et ça demande tout un travail algébrique pour arriver à dire que ce raccourci d’écriture est légitime.
Et je n'ai pas besoin de rentrer dans ce niveau de détail pour expliquer que ce sont les classes Letlang qui déterminent quels objets sont inclus, et non l'inverse.
Pour les espaces vectoriels tu es obligé de faire la distinction. Parler de 42 comme d’un vecteur ça veut rien dire, tu voulais probablement dire : 42 = 42 · 1 où le gras est un vecteur, en admettant que tu prennes la base canonique. La structure de l’espace vectoriel R n’est pas celle du corps R (le 42 non-gras : c’est le scalaire, c’est une coordonnée qui appartient par définition au corps R, le 42 gras : c’est un vecteur, il appartient au R-espace vectoriel R). Le 42 que tu as donné c’est la coordonnée du vecteur : pour ce faire, tu as considéré R muni d’une structure de (corps-R)-espace vectoriel, avec une base qui plus est.
C’est une erreur classique que de confondre les coordonnées d’un vecteur et le vecteur lui-même.
Je me demande si tu as lu la même chose que j'ai écrit. A aucun moment je ne parle de 42 comme étant un vecteur.
En vrai la seule mention de vecteur dans la spec c'est :
To reduce code duplication, a class can require type parameters:
class vector<T>(v: {x: T, y: T});
According to the above definition:
{x: 0, y: 0} is vector<int> = true;
{x: 0, y: 0} is vector<string> = false;
J'insiste sur le according to the above definition.
Les entiers, les nombres à virgule flottante, la définition de vecteur ci-dessus, et beaucoup de choses en informatique, n'ont pas grand chose à voir avec leur contrepartie mathématique.
Dans cette spec, je parle constamment de la structure des données, et de la définition des collections qui les contiennent. Je fais un rapide parallèle avec la théorie des ensembles ou c'est la définition de la collection qui détermine la structure des objets qu'elle contient.
Alors oui, la partie mathématique n'est pas la plus rigoureuse qui soit, mais ce n'est pas le but en fait, le but c'est de présenter un concept.
Le public auquel je m'adresse n'est pas forcément mathématicien, donc un peu de vulgarisation et quelques raccourcis, ça ne fait de mal à personne.
Le vrai mathématicien lira ça et se dira "oui, bon c'est un peu simplifié et pas très rigoureux, mais soit".
[^] # Re: théorie des ensembles pas naives
Posté par David Delassus (site web personnel) . En réponse au journal [Letlang] Et si on rédigeait la spec ?. Évalué à 4.
Utilité de ce commentaire ?
En quoi c'est pas pertinent ? Je parle de l'inspiration derrière le système de type afin de présenter le système de type justement qui diffère de la plupart des autres langages de programmation.
Il n'y a pas de "type" au sens informatique du terme. Le "type" au sens mathématique du terme c'est l'appartenance à une collection muni ou non d'opérations. Et un objet n'a pas un unique type car c'est la définition de la collection qui détermine cette appartenance.
Mais en pratique c'est le cas. x et y désignent tout deux le même objet qui, par la définition de Q et R, appartient aux 2 ensembles.
Et je n'ai pas besoin de rentrer dans ce niveau de détail pour expliquer que ce sont les classes Letlang qui déterminent quels objets sont inclus, et non l'inverse.
Je me demande si tu as lu la même chose que j'ai écrit. A aucun moment je ne parle de
42comme étant un vecteur.En vrai la seule mention de vecteur dans la spec c'est :
J'insiste sur le according to the above definition.
Les entiers, les nombres à virgule flottante, la définition de vecteur ci-dessus, et beaucoup de choses en informatique, n'ont pas grand chose à voir avec leur contrepartie mathématique.
Dans cette spec, je parle constamment de la structure des données, et de la définition des collections qui les contiennent. Je fais un rapide parallèle avec la théorie des ensembles ou c'est la définition de la collection qui détermine la structure des objets qu'elle contient.
Alors oui, la partie mathématique n'est pas la plus rigoureuse qui soit, mais ce n'est pas le but en fait, le but c'est de présenter un concept.
Le public auquel je m'adresse n'est pas forcément mathématicien, donc un peu de vulgarisation et quelques raccourcis, ça ne fait de mal à personne.
Le vrai mathématicien lira ça et se dira "oui, bon c'est un peu simplifié et pas très rigoureux, mais soit".
https://link-society.com - https://kubirds.com - https://github.com/link-society/flowg