C’est un système de typage nominal alors finalement. Le type est déterminé par le fait que tu ait fait passer la valeur par un constructeur du type, du coup tu peux lui coller l’étiquette « entier ». Si tu as une valeur de type nombre dont il serait possible avec un démonstrateur qu’elle est nécessairement un entier, elle ne sera pas déterminée comme tel comme ça pourrait l’être avec un système structurel de type (le type n’est pas donné par une étiquette de type mais par la forme/les propriétés de l’objet, cf. Système_structurel_de_types ). C’est quelque chose qui est assez classique en typage finalement, un constructeur d’un type apporte une preuve que certaines propriétés du type sont bien garanties. Un constructeur d’un type « liste triée » par exemple pourrait appliquer un tri sur une liste non triée en garantissant que le résultat est bien trié, et la propriété est garantie dans le système de type parce que la liste a bien le type « liste triée », qui permet de tracer la propriété finalement.
Tu dois avoir des « constructeurs » qui garantissent qu’une valeur de ton type a bien les bonnes propriétés. Et « int » ici c’est un sous-type de nombre dans le sens ou tu peux mettre un « int » dans n’importe quel contexte ou tu peux mettre un nombre, avec une relation de sous-typage qui est explicitement spécifiée. cf. Principe de substitution de Liskov.
[^] # Re: théorie des ensembles pas naives
Posté par thoasm . En réponse au journal [Letlang] Et si on rédigeait la spec ?. Évalué à 3.
C’est un système de typage nominal alors finalement. Le type est déterminé par le fait que tu ait fait passer la valeur par un constructeur du type, du coup tu peux lui coller l’étiquette « entier ». Si tu as une valeur de type nombre dont il serait possible avec un démonstrateur qu’elle est nécessairement un entier, elle ne sera pas déterminée comme tel comme ça pourrait l’être avec un système structurel de type (le type n’est pas donné par une étiquette de type mais par la forme/les propriétés de l’objet, cf. Système_structurel_de_types ). C’est quelque chose qui est assez classique en typage finalement, un constructeur d’un type apporte une preuve que certaines propriétés du type sont bien garanties. Un constructeur d’un type « liste triée » par exemple pourrait appliquer un tri sur une liste non triée en garantissant que le résultat est bien trié, et la propriété est garantie dans le système de type parce que la liste a bien le type « liste triée », qui permet de tracer la propriété finalement.
Tu dois avoir des « constructeurs » qui garantissent qu’une valeur de ton type a bien les bonnes propriétés. Et « int » ici c’est un sous-type de nombre dans le sens ou tu peux mettre un « int » dans n’importe quel contexte ou tu peux mettre un nombre, avec une relation de sous-typage qui est explicitement spécifiée. cf. Principe de substitution de Liskov.