J'avais vu passer cet article sur le planet OCaml, mais comme je ne suis pas un fin connaisseur de Haskell je n'y avais pas prêté attention plus que cela. Alors dans le fond, je suis d'accord vous avez raison, la catégorie Hask n'existe pas, et donc stricto sensu l'énoncé n'a formellement aucun sens. Pour reprendre sa comparaison avec les séries, c'est comme si ils affirmaient que toutes les séries étaient convergentes, d'où sa raillerie avec la question d'approximer à la quatrième décimale la valeur de la série 1 + 1/2 + 1/3 ....
Néanmoins, si l'on se limite aux calculs qui terminent (i.e. aux fonctions totales sans prendre en compte les fonctions partielles) les significations semblent se recouper en un certain sens. Du moins c'est ce que j'ai compris de l'article Fast and loose reasoning is morally correct que j'ai rapidement survolé. D'ailleurs dans un addendum à son article, Andrej Bauer ne semble pas remettre en cause cette approche :
Nor am I objecting to "fast & loose" mode of thinking while investigating a new idea in Haskell, that is obviously quite useful as well. I am objecting to:
The fact the the Haskell wiki claims there is such a thing as "the category Hask" and it pretends that everything is ok.
The fact that some people find it acceptable to defend broken mathematics on the grounds that it is useful. Non-broken mathematics is also useful, as well as correct. Good engineers do not rationalize broken math by saying "life is tough".
[^] # Re: Le code impératif
Posté par kantien . En réponse au sondage Ce que je déteste le plus en informatique / programmation / codage c'est... :. Évalué à 1.
Eh ! tu sodomises du diptère là. :-P
J'avais vu passer cet article sur le planet OCaml, mais comme je ne suis pas un fin connaisseur de Haskell je n'y avais pas prêté attention plus que cela. Alors dans le fond, je suis d'accord vous avez raison, la catégorie Hask n'existe pas, et donc stricto sensu l'énoncé n'a formellement aucun sens. Pour reprendre sa comparaison avec les séries, c'est comme si ils affirmaient que toutes les séries étaient convergentes, d'où sa raillerie avec la question d'approximer à la quatrième décimale la valeur de la série
1 + 1/2 + 1/3 ....Néanmoins, si l'on se limite aux calculs qui terminent (i.e. aux fonctions totales sans prendre en compte les fonctions partielles) les significations semblent se recouper en un certain sens. Du moins c'est ce que j'ai compris de l'article Fast and loose reasoning is morally correct que j'ai rapidement survolé. D'ailleurs dans un addendum à son article, Andrej Bauer ne semble pas remettre en cause cette approche :
Ce qu'il a peut être rajouté après ce commentaire d'Edward Kmett.
Pour ce qui est des objections d'Andrej, elles peuvent effectivement se défendre et se comprendre.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.