Re: Reason

[^] # Re: Reason

Posté par kantien le 18 août 2017 à 11:31. En réponse à la dépêche OCaml 4.04 et 4.05. Évalué à 2. Dernière modification le 18 août 2017 à 11:35.
Concernant les littéraux, je ne comprends pas pourquoi il sont considéré différemment du type.

En gros si tu as
i : int
i + 1

i + 1 est ok, uniquement car on détermine que 1 est d'un type entier.

Je ne vois toujours pas où tu veux en venir, et ce que tu veux dire par « les littéraux sont considérés différemment du type ». Le langage possède des types primitifs comme int, float, char ou string et l'on utilise des littéraux pour construire des valeurs de ces types.
```
1, 2.5, 'c', "type";;
- : int * float * char * string = (1, 2.5, 'c', "type")
```
Pour ton exemple, le type checker arrive bien à la conclusion :
```
i : int, 1 : int, + : int -> int -> int |- i + 1 : int
```
qu'est-ce qui te chagrine là-dedans ? Que le compilateur considère que 1 : int ? Mais c'est là le principe des types primitifs et des littéraux.

Or a part dans fonctionnalité de généricité, le type n'est jamais une variable. C'est chiant dans ingénierie des modèles, tu ne peux pas prévoir un modèle de plus haut niveau, qui sera utilisé pour en faire un de plus petit niveau en définissant le type de certain donné par exemple. Ce genre de problème se contourne en réinventant une sorte de typage depuis le modèle de haut niveau, mais c'est moche et lourd. De plus, la vérification des types doit être réécrites.

Ta question se situe peut-être ici. Un type est bien une variable dans le cas de la généricité : les types paramétriques sont des fonctions des types vers les types, c'est le principe des constructeurs des variants :
```
type 'a list =
 | [] : 'a list
 | (::) : 'a * 'a list -> 'a list
```
ici on a une fonction récursive, définie par cas, à un paramètre des types dans les types qui définie le type des listes chaînées.

Ce qui te pose problème, c'est quoi ? Que l'on n'ait pas de fonction des termes dans les types ? Là où il y a des fonctions des termes (ou valeurs) dans les termes et des fonctions des types dans les types ? Mais ça c'est le typage dépendant, et il faut passer à Coq. Ou alors je n'ai vraiment pas compris ta question.

Pour le reste, ne connaissant pas les domaines de l'ingénierie des modèles, des schéma XML ou UML, je ne peux rien en dire. Il faudrait que tu présentes un cas simple et concret, et non des généralités, pour que je comprennes où tu veux en venir.

Réponse bien complète :)

Pour un kantien, la complétude est une quête sans relâche. Dans sa dépếche sur Coq 8.5, Perthmâd signalait que, en vertu de la correspondance preuve-programme, le théorème de complétude de Gödel (que j'ai mentionnait précédemment) correspondait à un décompilateur (ou désassembleur). Kant¹, de son côté, ce n'est pas du code mais la structure formelle de l'esprit humain qu'il a désassemblé, selon un procédé analogue à celui qui se trouve à la base du lambda-calcul typé. :-)
1. je signale, au passage, que ce n'est pas moi mais Dinosaure qui a mis l'image sur la Critique de la Raison Pure dans le corps de la dépêche. ↩
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

[^] # Re: Reason