3. THÉORIE DES TYPES
Le chapitre 2 a construit l'appareil catégorique ; celui-ci en tire le système que le développeur écrit. Il n'y ajoute aucune construction : une seule décision, P2, épuise la question — tout type de K7PL est le produit d'une modalité d'usage et d'une contrainte de valeur, variant indépendamment l'une de l'autre. La modalité, trace au niveau des types de la stratification en trois fragments (§2.2), détermine si une ressource se copie librement, s'abandonne sans y avoir touché, ou doit être consommée exactement une fois. La contrainte de valeur ne dit rien de l'usage et tout du contenu : taille, intervalle, état, protocole, dimension physique. Aucune des deux ne conditionne l'autre — sous la seule condition de séparation posée par P2, que le §3.2 respecte en n'admettant que des indices exclus du suivi de ressource. De chaque notion, ce chapitre ne retient que ce qu'elle est en tant que type ; la manière dont elle s'exécute relève du chapitre 4, séparation qui prolonge au niveau du document l'orthogonalité qu'il construit au niveau des types.