kantien a écrit 1225 commentaires

C'est comme pour n'importe quel outil. La responsabilité va sur le propriétaire sauf si l’outil a un défaut de conception, comme pour les voitures actuelles…

Le problème ne se pose même pas. Personne n’achèterait une voiture qui conduit comme ça.

Personne n'achèterait une voiture pour laquelle ils seraient considérés comme responsables en cas d'accident (surtout s'il cause la mort d'un tiers) alors qu'ils ne peuvent rien y faire. ;-)

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

S'il s'agissait de C j'aurais tendance à penser pareil, mais les map ou fold sur des listes deviennent des itérations avec range sur un tableau en Go […]

Ou alors, pour être plus générique sur la conception des itérateurs, utiliser des foncteurs applicatifs : The Essence of the Iterator Pattern.

Pour les types somme, je suis assez d'accord, mais c'est pas intrinsèquement fonctionnel comme truc, je dirais.

Effectivement, voir le chapitre 1 de ce cours de programmation avancée pour la comparaison entre Java et OCaml sur la manière de définir des types algébriques.

La seule construction que je ne vois pas comment réaliser à la fois efficacement et de façon commode dans un langage impératif un peu haut-niveau, c'est la récursivité terminale entre fonctions mutuellement récursives (comme truc approchant, je vois que le retour de pointeur vers une fonction, qui a le défaut de faire des sauts calculés non prévisibles).

Avec des goto ? :-P

Ok, ---> [] …

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

En quoi le passage en SARL est une obligation ?

Je ne comprends pas ton interrogation. Le statut de Société Anthropomorphique des Rascasses et Limandes était bien sûr le plus adapté pour la SOLE (Search Of Learning Events).

Pour le chiffre d'affaire qui semble t'inquiéter, le statut prévoit explicitement que s'il est de 42 et que la SOLE réussi à le décomposer en facteurs premiers (exploit inédit à ce jour) la SARL sera exonérée de charges ad vitam æternam pour service rendu à la patrie : cela évitera aux juges d'avoir à demander les clés de chiffrement.

Nul doute qu'à partir de l'excellence de la base de données dont dispose la SOLE, elle mènera a bien cet exploit. Il paraîtrait même qu'elle aurait déjà trouvé les facteurs 7 et 3 en s'écriant : « en ce septième jour de la semaine, dimanche de Pâques, louons la sainte trinité notre Père, son Fils et le Saint Esprit et célébrons la résurrection de notre Seigneur ». L'équipe en charge de la superviser redoute tout de même une possible dérive vers un délire mystique et cabalistique : une enquête est en cours.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

La communauté scientifique est perplexe.

Afin de lever ses doutes, la communauté scientifique a demandé à l'IA de se représenter elle-même :

Le verdict n'a pas fait une plie : nous avons bien affaire à une intelligence de tout premier ordre. Le risque est grand que l'être humain soit bientôt déclaré obsolète.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

étrange, chez moi il n'y avait pas de raccourci défini…

Aller dans le menu de configuration du clavier, chercher « Masquer toutes les fenêtres normales » dans la section navigation, puis définir le raccourci à Super + D.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Pourtant il doit y avoir une façon de faire cela…j'ai juste jamais cherché!

Super + h pour cacher (hide) une fenêtre.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Après réflexion, vu les contraintes du programme, le mieux serait sans doute de faire :

stty raw -echo # raw mode plus générique que-icanon, et sans echo sur la sortie standard

avant de rentrer dans la boucle, et :

stty sane

pour rétablir le terminal dans un état sain avant de quitter le programme (cf man stty pour les explications).

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Concernant la récursivité en OCaml, y a-t-il une limitation du nombre d'appel récursif comme dans la plupart des langages impératifs ?

Absolument aucune limitation si les appels récursifs sont terminaux : il se font alors en espace constant sur la pile. Voir ma réponse du dessous à gndl.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Kantien pour sa brillante réponse.

Merci.

C’est cette progressivité qui me manque souvent dans la documentation sur OCaml.

Tu parles de la documentation officielle ? Celle-ci est plus un manuel de référence du langage qu'une initiation aux principes de la programmation fonctionnelle.

La traduction de la boucle while que j'ai faite relève des principes généraux de la programmation fonctionnelle. C'est pour cela que j'avais donné un lien vers un de mes commentaires sur le journal de la version de taptempo en Emacs Lisp. Une personne cherchait à écrire la fonction factorielle de manière récursive terminale et ne savait pas comment faire. Il avait écrit la version naïve :

let rec fact_non_tailrec = function
| 0 -> 1
| n -> n * fact_non_tailrec (n - 1)

qui génère un dépassement de pile sur de grandes entrées :

fact_non_tailrec 100_000_000;;
Stack overflow during evaluation (looping recursion?).

La version impérative pour une telle fonction, à base de boucle for, est la suivante :

let fact_for_loop n =
  let res = ref 1 in
  for i = n downto 1 do res := !res * i done;
  !res

La version fonctionnelle avec récursion terminale consiste donc à utiliser un boucle avec un accumulateur, comme dans la version impérative :

let factorielle n =
  let rec loop res = function
  | 0 -> res
  | n -> loop (n * res) (n-1)
  in loop 1 n

Dans les deux versions, impérative et fonctionnelle, la boucle dépend de l'entrée n. Mais, dans la version fonctionnelle, l'accumulateur est également un paramètre de la boucle, là où c'est une variable globale pour celle-ci dans le cas impératif.

Pour l'autre transformation du code, là c'est plutôt une astuce propre aux langages fonctionnels qui permettent d'avoir des opérateurs binaires infixes, donc hors famille Lisp et leur folie des parenthèses. L'idée étant que dans une telle situation :

step1 x; step2 x; step3 x

on puisse « factoriser » la variable sur laquelle on effectue notre séquence de transformation :

(step1 & step2 & step3) x
(* ou en chaînant à la manière d'une pipeline *)
x |- step1 |- step2 |- step3

Ici, il faut pouvoir définir les opérateurs d'ordre supérieur & et |-, ce que peut faire n'importe quel langage fonctionnel, mais leur utilité réside essentiellement dans le fait qu'on les utilise de manière infixe, ce qui fournit du sucre syntaxique à cette approche.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Comme tu es plus habitué au paradigme impératif, je donne ci-dessous la boucle while équivalente à mon code avec une fonction récursive, puis je donne une explication pour passer de l'un à l'autre.

(*
  valeurs impératives modifiées pendant la boucle,
  on les définit à l'éxtérieur avant de rentrer dedans
*)
let samples = Sample.create sample_size in
let stamp = ref (Mtime_clock.now ()) in
let key_pressed = ref (try input_char stdin with End_of_file -> 'q') in

(* on rentre dans la boucle *)
while !key_pressed <> 'q' do
  (* on ne fait quelque chose qu'en cas d'appui sur 'enter' *)
  if !key_pressed = '\n' then begin
    let new_stamp = Mtime_clock.now () in
    let elapsed = Mtime.(Span.to_s (span !stamp new_stamp)) in

    (* logique de mise à jour de la variable `samples` *)
    if elapsed > reset_delay then Sample.reset samples;
    Sample.add new_stamp samples;

    (* on affiche le message adapté *)
    show_bpm samples;

    (* mise à jour de la variable `stamp` *)
    stamp := new_stamp;
  end;
  (* mise à jour de la variable `key_pressed` *)
  key_pressed := try input_char stdin with End_of_file -> 'q'
done;

Le principe d'une boucle while, comme illustré dans cet exemple, est d'être une procédure qui modifie par effet de bords certaines variables qui lui sont globales (ici essentiellement samples et stamp) tant qu'une condition est satisfaite (ici, tant que l'on n'a pas appuyé sur q ou que l'entrée standard est n'est pas au bout). En tant que telle, du point de vue d'OCaml, c'est une expression qui a une valeur (comme n'importe quelle expression du langage) de type unit : ce type ne contient qu'une seule valeur (on parle de type singleton) notée (), c'est la valeur qui ne contient aucune information.

Pour transformer cette boucle en une fonction récursive, il faut d'abord qu'elle retourne la même valeur, à savoir (), lorsqu'elle termine. Ensuite, les variables globales sur laquelle opérait la boucle sont transformées en paramètres de la fonction : elles ne seront plus globales à la boucle, mais locales. On commence donc par écrire :

let rec loop stamp samples =

Ensuite, il faut exprimer la condition d'arrêt de la boucle. Celle-ci dépend du caractère que l'on lit sur l'entrée standard, d'où :

let rec loop stamp samples = match input_char stdin with

On fait alors une étude de cas, à la manière d'un switch, en commençant par dire quand la fonction termine (et qui renvoie alors ()) :

let rec loop stamp samples = match input_char stdin with
(* cas de fin de boucle *)
| exception End_of_file
| 'q' -> ()

Vient ensuite le cœur de la logique de la boucle, ce qui se passe quand on a appuyé sur enter :

let rec loop stamp samples = match input_char stdin with
(* cas de fin de boucle *)
| exception End_of_file
| 'q' -> ()
(* on a pressé 'enter' *)
| '\n' ->
  (* on remet la même logique qu'avec la boucle while *)
  let new_stamp = Mtime_clock.now () in
  let elapsed = Mtime.(Span.to_s (span !stamp new_stamp)) in

  (* logique de mise à jour de la variable `samples` *)
  if elapsed > reset_delay then Sample.reset samples;
  Sample.add new_stamp samples;

  (* on affiche le message adapté *)
  show_bpm samples;

  (* ici on ne met pas à jour la variable stamp mais
     on relance la boucle avec les nouveux paramètres *)
  loop new_stamp samples

Il reste enfin à traiter le cas où l'on a appuyé sur une autre touche : on ne fait rien et on relance la boucle avec les mêmes paramètres

let rec loop stamp samples = match input_char stdin with
(* je ne réécris pas la gestion des autres cas *)

(* cas par défaut : on boucle sans rien changer *)
| _ -> loop stamp samples

Maintenant que le corps de la fonction est écrit, il ne reste plus qu'à l'appeler pour lancer la boucle. Pour ce faire, on appelle la fonction avec, pour paramètres, les valeurs initiales des variables globales de la boucle while :

let rec loop stamp samples = match input_char stdin with
(* 
  bla bla
  bla bla
*)
in loop (Mtime_clock.now ()) (Sample.create sample_size)

Voilà le principe général pour transformer une boucle while en fonction récursive : on transforme les variables globales de la boucle en variables locales, et à chaque tour on lui passe les nouvelles valeurs.

Ceci étant, ce genre d'approche n'est pas propre au paradigme fonctionnel, mais ce dernier en fait un usage omniprésent et c'est la route vers la pureté (absence d'effets de bords)¹. Pour l'instant, la variable samples fonctionne toujours pas effet de bords et, dans le message précédent, j'ai juste modifié l'écriture de sa logique de mise à jour en utilisant une approche par pipe avec le code :

samples
|- (if elapsed > reset_delay then Sample.reset else ignore)
|- Sample.add new_stamp
|- show_bpm
|> loop new_stamp

Mais si, à la place d'une structure impérative, j'utilisais une structure purement applicative, j'aurais juste à changer les deux premiers combinateurs de tuyaux : un pipe |> au lieu d'un T |- et utiliser la fonction identity au lieu de ignore

samples
|> (if elapsed > reset_delay then Sample.reset else identity)
|> Sample.add new_stamp
|- show_bpm (* ici on log donc on utilise toujours le tee *)
|> loop new_stamp

Derrière cette vision par pipeline, il y a une notion élémentaire de mathématique (bon c'est pas du niveau primaire, mais début de lycée ;-), à savoir la composition de fonction.

que l'on peut écrire (la pipeline est assez visible sur le diagramme) :

fun x -> x |> f |> g |> h

L'opérateur de composition est une opérateur d'ordre supérieur : il prend deux fonctions en entrée et en renvoie une en sortie; raison pour laquelle il a une place centrale de le paradigme de la programmation fonctionnelle. Que peux-t-on faire avec une fonction ?

• les utiliser, ça on le fait dans tous les langages de la même façon ;
• les composer, ça c'est plus simple à écrire dans un langage fonctionnel.

J'espère que ces explications t'aideront un peu mieux à comprendre certains principes élémentaires à la base du paradigme fonctionnel.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Comme les compilateurs qui se respectent et qui se compilent eux-mêmes, n'importe quelle version d'upt pourra packager toutes les autres y compris elle-même. :-D

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Cela étant tu devrais peut être faire un appel à stty icanon avant de quitter ton programme, pour remettre le terminal dans sa configuration initiale.

Pour l'option echo, tu peux jouer avec cette commande dans ton terminal :

$ stty -echo

Attention : après on ne voit plus à l'écran ce que l'on tape (pratique pour la saisie d'un mot de passe ;-), il faut taper à l'aveugle la commande :

$ stty echo

pour remettre les choses en ordre. :-)

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Seconde erreur de ma part : ce n'est pas un appel récursif terminal… Je ne sais pas encore comment écrire ça.

Avec un accumulateur ;-)
Je ne suis pas un expert en Elisp, mais ça doit ressembler à cela :

(defun fact-tailrec (n acc)
  "Factorielle récursive terminale"
  (if (= n 0)
     acc
     (fact-tailrec ((- n 1) (* n acc)))))

(defun factorielle (n)
   fact-tailrec (n 1))

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

la réponse est dans le commentaire lié plus haut: stty -icanon désactive le buffering de STDIN, j'image qu'il est bufferisé pour des raisons de performance à l'origine

C'est le fonctionnement canonique (d'où le nom de l'option ;-) de l'entrée standard d'un terminal dans les systèmes Unix. man termios pour de plus amples informations (en désactivant la fonction echo, l'entrée standard ne renvoie pas ce qu'elle reçoit sur la sortie standard, par exemple).

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Merci, je vais étudier ça de près.

Dans ce cas, je te propose la version suivante de la boucle principale (dans une approche similaire à celle en Elixir et ce que l'auteur à appeler flow programming).

let rec loop stamp samples = match input_char stdin with
| exception End_of_file -> ()
| 'q' -> ()
| '\n' ->
  let new_stamp = Mtime_clock.now () in
  let elapsed = Mtime.(Span.to_s (span stamp new_stamp)) in    
  samples
  |- (if elapsed > reset_delay then Sample.reset else ignore)
  |- Sample.add new_stamp
  |- show_bpm
  |> loop new_stamp
| _ -> loop stamp samples
in loop (Mtime_clock.now ()) (Sample.create sample_size);

Ici c'est dans la même veine que le code Rust que tu ne comprenais pas : c'est à base de pipe (on connecte les flux d'entrée et de sortie de fonctions). Il y a deux types de connecteurs de flux sous forme d'opérateurs infixes : |- qui est proche de la commande unix tee (d'où le choix du symbole) et le |> qui fonctionne comme le pipe | du shell.

Si tu comprends cette commande, alors c'est bon :

$ (for i in $(seq 6); do echo; sleep 0.5; done) | ./taptempo | tee log1 | grep bpm | tee log2 | cut -d' ' -f2,3
120 bpm
120 bpm
120 bpm
120 bpm
120 bpm

$ cat log1
Appuyer sur la touche entrée en cadence (q pour quitter).

[Appuyer encore sur la touche entrée pour lancer le calcul du tempo...]
Tempo: 120 bpm
Tempo: 120 bpm
Tempo: 120 bpm
Tempo: 120 bpm
Tempo: 120 bpm

Au revoir !

$ cat log2
Tempo: 120 bpm
Tempo: 120 bpm
Tempo: 120 bpm
Tempo: 120 bpm
Tempo: 120 bpm

on chaîne les commandes, et on utilise tee pour faire un log de résultats intermédiaires mais sans casser le flux. Comme dans cet exemple OCaml :

let pipeline str =
  str
  |- Printf.printf "la chaîne est: \"%s\"\n"
  |> String.trim
  |- Printf.printf "on a retiré les espaces: \"%s\"\n"
  |> String.length
  |- Printf.printf "la longueur de la chaîne tronquée est: %i\n"
  |> succ
  |> (fun x -> 3 * x)
;;
val pipeline : string -> int = <fun>

on prend une chaîne, on lui retire les espaces en préfixe et suffixe (String.trim), on calcule la longueur de la chaîne ainsi obtenue (String.length) puis on effectue des calculs sur cette valeur entière, le tout en faisant quelques commandes de log entre temps. Exemple d'usage :

pipeline "   hello world !   ";;
la chaîne est: "   hello world !   "
on a retiré les espaces: "hello world !"
la longueur de la chaîne tronquée est: 13
- : int = 42

L'opérateur infixe |- se définit tout simplement ainsi :

(* on applique f à x, puis on retourne x pour pouvoir chaîner *)
let (|-) x f = (f x : unit); x;;
val ( |- ) : 'a -> ('a -> unit) -> 'a

j'ai juste mis une contrainte de type sur la sortie de f de telle sorte que :

x |- step1 |- step2 |- step3

(* soit bien équivalent à *)

step1 x; step2 x; step3 x

Maintenant, si on reprend la partie du code qui correspond au traitement à effectuer lors de l'appui sur la touche enter :

let new_stamp = Mtime_clock.now () in
let elapsed = Mtime.(Span.to_s (span stamp new_stamp)) in    
samples
|- (if elapsed > reset_delay then Sample.reset else ignore)
|- Sample.add new_stamp
|- show_bpm
|> loop new_stamp

On calcule un nouvelle horodatage et le temps écoulé (en secondes) depuis le dernier appui sur enter; ensuite on enchaîne les traitements sur la file des horodatages :

• si le temps écoulé est supérieur au délai de réinitialisation alors on reset, sinon on ne fait rien ;
• on ajoute l'horodatage à la file (ce qui met à jour, dans la structure, la valeur du tempo) ;
• on affiche le tempo ou le message qui dit d'appuyer une nouvel fois pour lancer le calcul (choix basé sur un type option contenu dans la structure[1]) ;
• on repart dans la boucle avec comme paramètres le nouvel horodatage et la file mise à jour.

C'est beau, c'est fin, ça se mange sans faim. :-)

---

[1]: en arrière plan, le type de la file d'horodatage est

type t = {
  size : int ; (* nombre max d'échantillons *)
  queue : Mtime.t Queue.t ; (* FIFO contenant les timestamps *)
  mutable tempo : float option ; (* Some tempo ou None *)
}

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Peux-tu m'expliquer comment le compiler et l'exécuter ?

Sans avoir à installer une partie des outils de développements OCaml, le plus simple est sans doute de passer par le gestionnaire de paquets de ta distribution. Sous Debian (ou dérivée), il te faudrait au minimum les paquets suivants :

$ apt install ocaml ocaml-findlib libgettext-ocaml

ensuite tu vas dans le répertoire des sources, et tu lances la commande suivante :

$ ocamlfind opt -package unix,gettext-camomile -linkpkg i18n.ml options.ml taptempocaml.ml -o taptempo

Par contre, chez moi, l'internationalisation ne marche pas : j'ai le texte en anglais. De plus, le flux de sortie standard n'est pas vidé sur certaines écritures : je ne vois rien avant d'avoir appuyer plusieurs fois sur enter. Tu peux corriger cela en rajoutant flush stdout; après ces deux lignes de taptempocaml.ml :

print_string(s_"Hit enter key for each beat (q to quit).\n");
flush stdout; (* <- à rajouter *)

(* ... *)
print_string(s_"[Hit enter key one more time to start bpm computation...]\n");
flush stdout (* <-  à rajouter mais pas besoin du `;' ici *)

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Ce qui serait super cool maintenant, c'est que quelqu'un, pas forcément toi, mette une version plus OCaml comme on en voit traîner régulièrement sur LinuxFr :)

Qu'entends-tu par plus OCaml ? Tu veux dire dans un style fonctionnel ? Là son code est fondamentalement impératif (le langage est multi-paradigme) et les traits impératifs se prêtent bien au problème. Ceci étant on pourrait ne pas mettre de boucle while, mais une fonction récursive à la place, du genre :

let rec loop time = match input_char stdin with
| exception End_of_file -> ()
| 'q' -> ()
| '\n' ->
  let new_time = Mtime_clock.now () in

  if Mtime.(Span.to_s (span time new_time)) > reset_delay
  then Sample.clear samples;

  Sample.add new_time samples; show_bpm samples; loop new_time
| _ -> loop time
in loop @@ Mtime_clock.now ();

c'est ce genre de code dont tu parles ? (ici j'utilise une horloge monotone et un module à ma sauce pour gérer la logique de calcul du tempo)

L'avantage que je vois, c'est que cela évite les imbrications, des fois dure à suivre, des if then else. Ici on est protégé des exceptions et seule la touche enter peut être appuyée en cadence. Sans cela, un test comme :

$ (for i in $(seq 6); do echo; sleep 0.5; done) | ./taptempo | grep bpm
Tempo: 120 bpm
Tempo: 120 bpm
Tempo: 120 bpm
Tempo: 120 bpm
Tempo: 120 bpm

générera une exception (non rattrapée) quand le flux d'entrée est fermé et, selon que l'on accepte ou non n'importe quel caractère, cela peut changer le résultat de celui-ci :

# seule la touche enter
$ (for i in $(seq 6); do echo 'taptempo'; sleep 0.5; done) | ./taptempo | grep bpm | wc -l
5

# n'importe quel caractère
$ for i in $(seq 6); do echo 'taptempo'; sleep 0.5; done) | ./taptempo | grep bpm | wc -l
53 # sans compter le calcul du tempo qui s'envole ;-)

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Les langages avec des vraies macros , comme Collin Lisp que je cite permettent de tout programmer de façon assez agréable. Par exemple avec cl-async, on peut presque réutiliser son code synchrone avec des promises, il suffit presque de changer les let en alet;)

Avec l'extension de syntaxe de Lwt aussi ;-).

Dans utop, il suffit de faire :

#require "lwt";;
#require "lwt.ppx";;

Pour une version avec bind, proche de la syntaxe NodeJS, où on passe la promesse à une fonction anonyme :

let main () =
  let open Lwt in
  Lwt_io.print "Entrer votre nom: " >>= fun () ->
  Lwt_io.(read_line stdin) >>= fun nom ->
  Lwt_io.printlf "Votre nom est: %s" nom
;;
val main : unit -> unit Lwt.t = <fun>

let () = Lwt_main.run (main ());;
Entrer votre nom: kantien
Votre nom est: kantien

La même, mais avec l'extension de syntaxe : on retrouve une forme proche de celle d'un code synchrone (les let x = e in sont remplacés par des let%lwt x = e in) :

let main () =
  let%lwt () = Lwt_io.print "Entrer votre nom: " in
  let%lwt nom = Lwt_io.(read_line stdin) in
  Lwt_io.printlf "Votre nom est: %s" nom
;;
val main : unit -> unit Lwt.t = <fun>

let () = Lwt_main.run (main ());;
Entrer votre nom: kantien
Votre nom est: kantien

Il y a une forme (à base de %lwt à rajouter) pour presque toutes les constructions syntaxiques du langage.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Tu penses (probablement) à une monade spécifique qui fait de la composition de fonctions.

Bah, c'est la monade identité, qui n'est pas spécialement la plus utile.

Par contre, je comprends pas trop où veut en venir Michaël : avec les monades et leur bind, on les utilise plutôt dans le sens inverse de la composition (à la manière du pipe du shell).

          f                 g
 A   ----------->  B   ----------->  C
 |                 |                 |
 |                 |                 |
 V      map f      V       map g     V
F(A) -----------> F(B) -----------> F(C)

Là j'ai trois types A, B et C et deux fonctions f : A -> B et g : B -> C. Si je les compose, j'obtiens une fonction de A vers C. On peut le dire en mode direct (à la mode mathématique) : applique g au résultat de f; ou en mode inverse : passe le résultat de f à g. La conception à la manière d'une pipeline, c'est de le voire comme sur le dessin en mode inverse : on écrit les traitements dans l'ordre où ils sont effectués (f puis g).

Après une monade, c'est un type paramétrique (ici F sur le dessin) avec certaines bonnes propriétés. Tout d'abord on doit pouvoir faire un map dessus : à partir de f : A -> B, on peut construire map f : F(A) -> F(B) qui respecte la composition. Si je compose f et g, puis que j'applique map, ou que j'applique map puis que je compose, on doit obtenir le même résultat.

Ensuite, pour que ce type paramétrique soit une monade, il faut pouvoir combiner une fonction A -> F(B) avec un autre B -> F(C) : ce sont les diagonales que l'on cherche à assembler. Mais pour ce faire, on utilise plutôt l'opérateur bind (ou >>= en notation infixe) qui prend une valeur de type F(A), une fonction de type A -> F(B) et renvoie une valeur de type F(B). C'est l'équivalent du pipe pour les monades : le pipe est à la composition de fonctions, ce que le bind est à la composition d'opérateurs monadiques.

(* on va de A vers C en composant f et g *)
x |> f |> g

(* 
   on va de F(A) vers F(C) via la monade
   f' et g' sont les fonctions en diagonales
*)
mx >>= f' >>= g'

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Difference between CLOCK_REALTIME and CLOCK_MONOTONIC? ;-)

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

D'ailleurs, je préfère la version verbeuse, je la trouve plus lisible ;)

C'est parce que la pipeline est courte. Il faut voir cette notation pointée de Rust comme le pipe | du shell : reader.next() | unwrap_or | map_err | map. Sur de longues pipelines, c'est plus simple à écrire et il vaut mieux laisser le compilateur inliner le tout plutôt que de le faire à la main (comme dans sa version verbeuse, qui contient d'ailleurs une erreur : le cas None doit retourner Ok(false) de type Result<Bool, String>).

En OCaml (j'étais bien obligé), on écrirait un code du genre :

next reader |> Option.default (Ok "q") |> Result.map_both (fun s -> s <> "q") format_error

Les patterns à base de map sont omniprésents dans le paradigme fonctionnel. Un type paramétrique à un paramètre (comme les options, les listes, les tableaux, les vecteurs…) est une fonction des types dans les types. Ainsi si j'ai une fonction qui transforme les objets du paramètre (disons des int en string), je peux la lifter pour opérer sur le type paramétrique (un peu comme une composition de fonction, si tu veux). Exemples :

(* un int optionnel devient un string optionnel *)
Option.map string_of_int (Some 1);;
- : string option = Some u"1"

(* une liste de ints devients une liste de strings *)
List.map string_of_int [1; 2; 3];;
- : string list = [u"1"; u"2"; u"3"]

(* un tableau de ints devient un tableau de strings *)
Array.map string_of_int [|1; 2; 3|];;
- : string array = [|u"1"; u"2"; u"3"|]

Le type Result est lui un type paramétrique à deux paramètres : on peut donc faire un map soit sur le type en paramètre de Ok, soit sur celui en paramètre de Err. Ce qui soit donne deux fonctions map (comme en Rust), soit une fonction map_both comme dans mon exemple en OCaml (ou bimap en Haskell) qui prend deux fonctions en paramètres (une pour chaque type).

(* la double map pour le type result *)
let bimap f g = function Ok x -> Ok (f x) | Error e -> Error (g e)

(* le unwrap_or comme en Rust *)
let unwrap_or d = function None -> d | Some x -> x

(* la pipeline comme en Rust *)
let pipeline x = 
  x
  |> unwrap_or (Ok "q")
  |> bimap (fun s -> s <> "q") ( Printf.sprintf "Houla y'a eu un truc: %s")

(* exemples de sortie *)
pipeline None;;
- : (bool, string) result = Ok false

pipeline (Some (Ok "f"));;
- : (bool, string) result = Ok true

pipeline (Some (Error "une erreur"));;
- : (bool, string) result = Error u"Houla y'a eu un truc: une erreur"

P.S : sinon sympa le journal, et comme depuis les derniers journaux sur la virgule flottante j'ai installé GNAT et GNAT Programming Studio je vais pouvoir regarder un code ADA idiomatique et jouer avec :-) (ravi de voir au passage qu'il y a des développeurs ADA qui comprennent l'encapsulation ;-).

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Pourquoi vous n'avez jamais trouvé un moyen d'éviter d'utiliser les insupportables opérateurs float (+.),(-.),(/.),(*.) ?

Il y a une proposition pour résoudre ce problème, et offrir bien plus de possibilité, sous la forme de modules implicites. Il y a eu une discussion sur le sujet sur le forum OCaml, et il reste des questions tant théoriques que pratiques (au niveau de l'implémentation) à résoudre avant de voir apparaître le système dans le langage.

Pour faire simple, l'idée est de passer par des modules de premières classes et, dans le cas de ces opérateurs, de définir, disons, un type de module pour les corps :

module type CORPS = sig
  type t
  val zero : t
  val one : t
  val add : t -> t -> t
  val sub : t -> t -> t
  val mul : t -> t -> t
  val div : t -> t -> t
end

puis à définir, disons une fonction add, qui opère sur n'importe quel corps et des valeurs du support du corps :

let add (type a) (module M : CORPS with type t = a) x y = M.add x y;;
val add : (module CORPS with type t = 'a) -> 'a -> 'a -> 'a = <fun>

Ici le corps à passer en paramètre est explicite et si on utilise l'alternative Batteries à la bibliothèque standard, on peut écrire :

add (module Float) 2.3 4.5;;
- : float = 6.8

L'idée étant de faire du module de première classe un paramètre implicite déterminé automatiquement par le compilateur en fonction du type des paramètres x et y. Ici comme ce sont des float, le compilateur cherchera dans son environnement au moment de l'appel à add un corps sur les float déclaré utilisable comme arguments implicites.

En attendant, si tu utilises Batteries tu peux écrire ton code sur les flottants via des open locaux :

let open Float.Infix in 2.3 + 4.5;;
- : float = 6.8

voir la définition du module Float.Infix :

#show_module Float.Infix;;
module Infix = BatFloat.Infix
module Infix :
  sig
    type bat__infix_t = float
    val ( + ) : float -> float -> float
    val ( - ) : float -> float -> float
    val ( * ) : float -> float -> float
    val ( / ) : float -> float -> float
    val ( ** ) : float -> float -> float
    val ( -- ) : float -> float -> float BatEnum.t
    val ( --- ) : float -> float -> float BatEnum.t
    val ( =~ ) : ?epsilon:float -> float -> float -> bool
  end

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Ltac est un bousin sans nom qui est la source d'un tas de problèmes, le genre de code qu'il suffit de regarder fixement pour faire péter un développement à l'autre bout de la planète.

Justement, au sujet de Ltac, vous avez des idées ou des pistes pour l'améliorer et faciliter l'écriture de tactiques ? Si on prend l'exemple de patrick_g :

Par exemple dans de nombreux articles de géométrie arithmétique ou de géométrie algébrique on peut voir des phrases du style : "Par un argument à la GAGA il est facile de voir que blabla".

il doit bien être possible d'écrire une tactique gaga, mais ce possible reste souvent « théorique », écrire une tactique finissant par rendre à moitié fou (j'ai jamais bien compris comment marchait le système).

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Et tu n'as pas parlé d'une partie qui me semble prendre de plus en plus de temps dans le monde académique : la recherche de financement.

Pour le langage développé au sein de sa nouvelle équipe, on trouve ces informations sur le site du langage. À l'origine, le projet fut financé par l'entreprise Boston Scientific spécialisé dans le matériel médical, puis par des fonds publics provenant de la National Science Foundation (équivalent américain du CNRS).

Je me demande, d'ailleurs, si le nom du langage (Abella) ne vient pas du premier financeur : l'entreprise a été cofondée par John Abele. Au départ (j'aime bien essayé de trouver l'origine des noms des projets) je pensais que le nom faisait référence au logicien de l'époque scolastique Pierre Abélard car il est souvent utilisé en théorie de la démonstration avec sa bien aimée Héloïse (comme dans l'article Formules valides, jeux et protocoles réseau qui utilise des principes identiques à ceux dont parle gasche dans son journal, mais pour la certification de protocoles réseau), mais l'hypothèse de John Abele me semble plus probable.

démystifier l'activité de recherche et montrer à quoi « ça sert » puisque l'on vit dans un monde où la finalité semble importante à beaucoup :-/

Il en a été de tout temps ainsi, et une citation du maître pour la route :-)

Il n'est point de connaissance qui soit superflue et inutile de façon absolue et à tous égards, encore que nous ne soyons pas toujours à même d'en apercevoir l'utilité. C'est par conséquent un objection aussi mal avisée qu'injuste que les esprits superficiels adressent aux grands hommes qui consacrent aux sciences des soins laborieux lorsqu'ils viennent demander : à quoi cela sert-il ? On ne doit en aucun cas poser une telle question quand on prétend s'occuper de science. À supposer qu'une science ne puisse apporter d'explication que sur un quelconque objet possible, de ce seul fait son utilité serait déjà suffisante. Toute connaissance logiquement parfaite a déjà quelque utilité possible : même si elle nous échappe jusqu'à présent, il se peut que la postérité la découvre. Si en cultivant les sciences on n'avait jamais mesuré l'utilité qu'au profit matériel qu'on pourrait retirer, nous n'aurions pas l'arithmétique et la géométrie. Aussi bien notre intelligence est ainsi conformée qu'elle trouve satisfaction dans la simple connaissance, et même une satisfaction plus grande que dans l'utilité qui en résulte. Platon l'avait déjà remarqué. L'homme y prend conscience de sa valeur propre; il a la sensation de ce qui se nomme : avoir l'intelligence. Les hommes qui ne sentent pas cela doivent envier les bêtes. La valeur intrinsèque que les connaissances tiennent de leur perfection logique est incomparable avec leur valeur extrinsèque, qu'elles tirent de leur application.

Emmanuel Kant, Logique

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

tu veux dire Inria? ^{^}

C'est une boutade au sein de l'Institut depuis qu'ils ont changé leur identité visuelle ?

En tout cas, gasche suit la graphie de sa nouvelle équipe — qui n'a peut être pas mis à jour sa page de présentation depuis le changement, à la lecture des dates qui y figurent.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.