La façon de comprendre la traduction entre de "truth" et "falsity" en termes de CS "type singleton" et "type vide" est que "A implique B est vraie" et "il existe une et une seule fonction de A vers B", correct?
Hum, ta phrase est un peu bancale grammaticalement et je ne comprends pas très bien où tu veux en venir. Je peux te justifier la définition calculatoire de « vrai » et « faux » comme suit. Il y a une et une seule preuve de « vrai », et donc « vrai » est l'équivalent sur le versant logique du type unit d'OCaml, disons (tu as l'air de pratiquer), i.e. le type algébrique à un seul constructeur (type unit = ()). De la même manière, on espère secrètement qu'il n'y a pas de preuve de faux, donc on définit faux comme le type vide, i.e. le type algébrique à zéro constructeurs (je ne crois pas que ça soit possible en OCaml pour des raisons débiles de parsing, mais tu peux l'encoder avec des GADTs).
Est-ce qu'il n'y a pas un poly que tu pourrais me recommander. Je suis mathématicien mais je ne suis pas très familier avec le domaine de la logique proprement dite ou la théorie des types, donc je pense que je pourrais arriver à profiter un peu d'un cours de DEA ou de Master.
Si tu aimes les catégories, tu peux tenter le HoTT book, même si je dois avouer que ne cautionne pas l'OPA qu'ont fait les homotopistes sur la théorie des types et le rebranding en « homotopique » de plein de choses qui existaient déjà dans la bête théorie des types. À part ça, dans la catégorie « bouquin moderne », je vois pas trop. Type Theory and Functional Programming a l'air pas trop mal à vue de nez.
[^] # Re: Le web
Posté par Perthmâd . En réponse au journal Qui fait des trucs "cools" en France et en Europe?. Évalué à 2.
Hum, ta phrase est un peu bancale grammaticalement et je ne comprends pas très bien où tu veux en venir. Je peux te justifier la définition calculatoire de « vrai » et « faux » comme suit. Il y a une et une seule preuve de « vrai », et donc « vrai » est l'équivalent sur le versant logique du type unit d'OCaml, disons (tu as l'air de pratiquer), i.e. le type algébrique à un seul constructeur (type unit = ()). De la même manière, on espère secrètement qu'il n'y a pas de preuve de faux, donc on définit faux comme le type vide, i.e. le type algébrique à zéro constructeurs (je ne crois pas que ça soit possible en OCaml pour des raisons débiles de parsing, mais tu peux l'encoder avec des GADTs).
Si tu aimes les catégories, tu peux tenter le HoTT book, même si je dois avouer que ne cautionne pas l'OPA qu'ont fait les homotopistes sur la théorie des types et le rebranding en « homotopique » de plein de choses qui existaient déjà dans la bête théorie des types. À part ça, dans la catégorie « bouquin moderne », je vois pas trop. Type Theory and Functional Programming a l'air pas trop mal à vue de nez.