Et par rapport à la logique, si j'ai bien compris l'origine du lambda calcul, c'est les incohérences de la théorie des ensembles qui ont donné la théorie des catégories (?) puis le lambda calcul, mais quel rapport ici, entre le typage est la logique. Le typage définit un ensemble de "vérité", et le compilateur vérifie la cohérence de l'ensemble ? Pourquoi les littéraux sont définit de manière spéciale par rapport au typage, c'est une question de facilité, ou est-ce qu'il y a une vrai différence de nature ?
[^] # Re: Reason
Posté par Nicolas Boulay (site web personnel) . En réponse à la dépêche OCaml 4.04 et 4.05. Évalué à 3.
Et par rapport à la logique, si j'ai bien compris l'origine du lambda calcul, c'est les incohérences de la théorie des ensembles qui ont donné la théorie des catégories (?) puis le lambda calcul, mais quel rapport ici, entre le typage est la logique. Le typage définit un ensemble de "vérité", et le compilateur vérifie la cohérence de l'ensemble ? Pourquoi les littéraux sont définit de manière spéciale par rapport au typage, c'est une question de facilité, ou est-ce qu'il y a une vrai différence de nature ?
"La première sécurité est la liberté"