Pour la version longue : voir ce commentaire que j'avais fait l'an dernier sur les principes de base du lambda-calcul typé. J'y comparais le typage de OCaml (qui est décidable, sauf sur quelques corner cases, d'où l'inférence de types) et celui de Coq qui lui ne l'est pas et donc le programmeur doit le dériver lui même explicitement, ce qui s'appelle faire une démonstration au sens mathématique du terme.
Pour la version courte : disons que le language des types c'est, grosso modo, celui de la logique propositionnelle du second ordre. C'est à dire que l'on a des variables propositionnelles : A, B, C..., l'implication logique A -> B (si A alors B), la conjonction A et B et la disjonction exclusive A ou B. L'implication : c'est le type des fonctions de A dans B; la conjonction : c'est les types produits, l'équivalent des struct du C; la disjonction : c'est les types sommes, les union du C mais en mieux.
On appelle ces deux genres de types, types sommes et types produits à cause de cette relation : A et (B ou C) <-> (A et B) ou (A et C). Ce qui donne une des définitions du concept d'algèbre de Boole au sens où l'entendent les mathématiciens : c'est un corps dans lequel tout élément est sont propre carré ((A et A) <-> A). L'algèbre a deux éléments {vrai, faux} étant la plus simple et la plus triviale de telles algèbres.
Par exemple, le type des listes : type 'a liste = Nil | Cons of 'a liste exprime une disjonction : c'est soit la constante propositionnelle Nil, soit une variable propositionnelle indexée par le type lui-même (ce qui fait que le type exprime une disjonction infinie, disjonction qui pour un type 'a donné est isomorphe à l'ensemble des entiers naturels 0 ou 1 ou 2 ou 3...). Pour les types produits, on peut prendre par exemple les points du plan : type point = {x:float; y:float}; c'est la donnée d'un intet d'un int, d'où la conjonction.
Ce qui fait qu'à l'arrivée, on tombe bien sur la logique des stoïciens.
Le principe d'application des fonctions, par exemple, c'est la régle de déduction logique dite du modus ponens : Si A alors B, or A, donc B. Règle que l'on écrit en logique propositionnelle : (A -> B) -> A -> B. À comparer avec le type inféré de la fonction suivante :
letapplyfx=fx;;valapply:('a->'b)->'a->'b=<fun>
L'inférence de type relève de la preuve automatique, Coq c'est de la preuve assistée par ordinateur, et les principes du typage du lambda-calcul proviennent tous de la théorie de la démonstration. Et donc coder en fonctionnel, c'est faire une preuve : le principe même de la correspondance de Curry1-Howard, ou correspondance preuve-programme. Le compilateur gueule, au niveau du typage, quand il considère qu'il y a un vice de forme dans la preuve.
le même Curry qui a donné son nom à la curryfication, et qui s'appelait Haskell Brooks Curry. ;-) ↩
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Jai: Language for game programmming
Posté par kantien . En réponse à la dépêche C++17, Genèse d’une version mineure. Évalué à 2.
Pour la version longue : voir ce commentaire que j'avais fait l'an dernier sur les principes de base du lambda-calcul typé. J'y comparais le typage de OCaml (qui est décidable, sauf sur quelques corner cases, d'où l'inférence de types) et celui de Coq qui lui ne l'est pas et donc le programmeur doit le dériver lui même explicitement, ce qui s'appelle faire une démonstration au sens mathématique du terme.
Pour la version courte : disons que le language des types c'est, grosso modo, celui de la logique propositionnelle du second ordre. C'est à dire que l'on a des variables propositionnelles :
A, B, C..., l'implication logiqueA -> B(si A alors B), la conjonctionA et Bet la disjonction exclusiveA ou B. L'implication : c'est le type des fonctions deAdansB; la conjonction : c'est les types produits, l'équivalent desstructdu C; la disjonction : c'est les types sommes, lesuniondu C mais en mieux.On appelle ces deux genres de types, types sommes et types produits à cause de cette relation :
A et (B ou C) <-> (A et B) ou (A et C). Ce qui donne une des définitions du concept d'algèbre de Boole au sens où l'entendent les mathématiciens : c'est un corps dans lequel tout élément est sont propre carré ((A et A) <-> A). L'algèbre a deux éléments{vrai, faux}étant la plus simple et la plus triviale de telles algèbres.Par exemple, le type des listes :
type 'a liste = Nil | Cons of 'a listeexprime une disjonction : c'est soit la constante propositionnelleNil, soit une variable propositionnelle indexée par le type lui-même (ce qui fait que le type exprime une disjonction infinie, disjonction qui pour un type'adonné est isomorphe à l'ensemble des entiers naturels0 ou 1 ou 2 ou 3...). Pour les types produits, on peut prendre par exemple les points du plan :type point = {x:float; y:float}; c'est la donnée d'unintet d'unint, d'où la conjonction.Ce qui fait qu'à l'arrivée, on tombe bien sur la logique des stoïciens.
Le principe d'application des fonctions, par exemple, c'est la régle de déduction logique dite du modus ponens : Si A alors B, or A, donc B. Règle que l'on écrit en logique propositionnelle :
(A -> B) -> A -> B. À comparer avec le type inféré de la fonction suivante :L'inférence de type relève de la preuve automatique, Coq c'est de la preuve assistée par ordinateur, et les principes du typage du lambda-calcul proviennent tous de la théorie de la démonstration. Et donc coder en fonctionnel, c'est faire une preuve : le principe même de la correspondance de Curry1 -Howard, ou correspondance preuve-programme. Le compilateur gueule, au niveau du typage, quand il considère qu'il y a un vice de forme dans la preuve.
le même Curry qui a donné son nom à la curryfication, et qui s'appelait Haskell Brooks Curry. ;-) ↩
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.