Le problème est que le type d'un objet, du point vue de la théorie des types, c'est une approximation (syntaxique) qui permet à travers un système de type de prouver des propriétés de programmes en temps borné.
De ce point de vue de là, les objets de Letlang ont un type unique. Le système de type de Letlang permet juste de construire un type comme une union de types pré-existants. Un système de type avec un produit, une union et des constructeurs de types n'est pas très original en soi.
Par contre, le manque de types sommes, récursifs ou algébriques est un choix de conception fort, et une lacune pour un système de type de mon point de vue.
Et je ne suis pas vraiment sûr de savoir comment se comporte la segmentation des types des valeurs en univers. Mais c'est pour partie parce que les règles de typage des univers ne sont pas décrit.
Par exemple, soit une valeur x de type t de l'univers 1, et une valeur y de type de u l'univers 2: quel est l'univers de (x,y)? À moins que (x,y) ne soit pas autorisé? Qu'en est-t-il du polymorphisme d'univers?
[^] # Re: théorie des ensembles pas naives
Posté par octachron . En réponse au journal [Letlang] Et si on rédigeait la spec ?. Évalué à 3. Dernière modification le 09 mai 2022 à 19:04.
Le problème est que le type d'un objet, du point vue de la théorie des types, c'est une approximation (syntaxique) qui permet à travers un système de type de prouver des propriétés de programmes en temps borné.
De ce point de vue de là, les objets de
Letlangont un type unique. Le système de type deLetlangpermet juste de construire un type comme une union de types pré-existants. Un système de type avec un produit, une union et des constructeurs de types n'est pas très original en soi.Par contre, le manque de types sommes, récursifs ou algébriques est un choix de conception fort, et une lacune pour un système de type de mon point de vue.
Et je ne suis pas vraiment sûr de savoir comment se comporte la segmentation des types des valeurs en univers. Mais c'est pour partie parce que les règles de typage des univers ne sont pas décrit.
Par exemple, soit une valeur
xde typetde l'univers 1, et une valeuryde type deul'univers 2: quel est l'univers de(x,y)? À moins que(x,y)ne soit pas autorisé? Qu'en est-t-il du polymorphisme d'univers?