Sommaire
Cher Nal,
Comme il faut bien un minimum de contenu sérieux aujourd’hui, histoire de faire diversion, je vais te parler de mes recherches sur la problématique print(1 + "3a"). Chaque langage/compilateur a sa façon de réagir sur le sujet, sa sensibilité, ses opinions ; des fois c’est juste une question de style, d’autres fois c’est des questions plus profondes qui émergent !
Voici donc les fruits de ces recherches.
Veux‐tu faire un print(1 + "3a"), s’il te plaît ?
Ceux qui te rejettent à l’exécution parce que Num + String, quoi
Ruby 1.8, c’est le point de vue coercition de types :
$ ruby18 -e 'puts 1 + "3a"'
-e:1:in `+': String can't be coerced into Fixnum (TypeError)
from -e:1
Avec Python, on a droit à la perspective de la surcharge d’opérateur :
$ python -c 'print(1 + "3a")'
Traceback (most recent call last):
File "<string>", line 1, in <module>
TypeError: unsupported operand type(s) for +: 'int' and 'str'
Pour Racket, c’est est une question bureaucratique de contrat non respecté !
$ racket -e '(printf "~s\n" (+ 1 "3a"))'
+: contract violation
expected: number?
given: "3a"
argument position: 2nd
other arguments...:
1
Guile, avare en paroles, se plaint d’un point de vue typage, tout en pointant le vilain "3a" du doigt cependant :
$ guile -c '(display (+ 1 "3a"))'
ERROR: In procedure +:
ERROR: Wrong type: "3a"
Avec Common Lisp (sbcl), on a droit à des hurlements, on a fait une erreur simple de typage ! Et les remontrances n’en finissent pas…
$ sbcl --noinform --non-interactive --eval '(print (+ 1 "3a"))'
Unhandled SIMPLE-TYPE-ERROR: Argument Y is not a NUMBER: "3a"
Backtrace for: #<SB-THREAD:THREAD "main thread" RUNNING {1002C06753}>
0: ((LAMBDA NIL :IN SB-DEBUG::FUNCALL-WITH-DEBUG-IO-SYNTAX))
1: (SB-IMPL::CALL-WITH-SANE-IO-SYNTAX #<CLOSURE (LAMBDA NIL :IN SB-DEBUG::FUNCALL-WITH-DEBUG-IO-SYNTAX) {1002C193FB}>)
2: (SB-IMPL::%WITH-STANDARD-IO-SYNTAX #<CLOSURE (LAMBDA NIL :IN SB-DEBUG::FUNCALL-WITH-DEBUG-IO-SYNTAX) {1002C193CB}>)
3: (PRINT-BACKTRACE :STREAM #<SYNONYM-STREAM :SYMBOL SB-SYS:*STDERR* {10001528B3}> :START 0 :FROM :INTERRUPTED-FRAME :COUNT NIL :PRINT-THREAD T :PRINT-FRAME-SOURCE NIL :METHOD-FRAME-STYLE NIL)
4: (SB-DEBUG::DEBUGGER-DISABLED-HOOK #<SIMPLE-TYPE-ERROR expected-type: NUMBER datum: "3a"> #<unavailable argument>)
5: (SB-DEBUG::RUN-HOOK *INVOKE-DEBUGGER-HOOK* #<SIMPLE-TYPE-ERROR expected-type: NUMBER datum: "3a">)
6: (INVOKE-DEBUGGER #<SIMPLE-TYPE-ERROR expected-type: NUMBER datum: "3a">)
7: (ERROR SIMPLE-TYPE-ERROR :DATUM "3a" :EXPECTED-TYPE NUMBER :FORMAT-CONTROL "~@<Argument ~A is not a ~S: ~2I~_~S~:>" :FORMAT-ARGUMENTS (SB-KERNEL::Y NUMBER "3a"))
8: (SB-KERNEL:TWO-ARG-+ 1 "3a")
9: (+ 1 "3a")
10: (SB-INT:SIMPLE-EVAL-IN-LEXENV (+ 1 "3a") #<NULL-LEXENV>)
11: (SB-INT:SIMPLE-EVAL-IN-LEXENV (PRINT (+ 1 "3a")) #<NULL-LEXENV>)
12: (EVAL (PRINT (+ 1 "3a")))
13: (SB-IMPL::PROCESS-EVAL/LOAD-OPTIONS ((:EVAL . "(print (+ 1 \"3a\"))") (:QUIT)))
14: (SB-IMPL::TOPLEVEL-INIT)
15: ((FLET #:WITHOUT-INTERRUPTS-BODY-83 :IN SAVE-LISP-AND-DIE))
16: ((LABELS SB-IMPL::RESTART-LISP :IN SAVE-LISP-AND-DIE))
unhandled condition in --disable-debugger mode, quitting
jq nous dit que ce qu’on lui demande est tout simplement impossible :
$ echo {} | jq '1 + "3a"'
jq: error (at <stdin>:1): number (1) and string ("3a") cannot be added
Pour K (kona), c’est une erreur de type pour +, mais on n’en saura pas plus.
$ k
K Console - Enter \ for help
1 + "3a"
type error
1 + "3a"
^
J voit là un problème de domaine et nous rajoute des espaces quelque part là où ça coince :
$ jc
1 + '3a'
|domain error
| 1 +'3a'
Ceux qui te rejettent à l’exécution, mais parce que « a » dans "3a"
Perl 6 voudrait bien essayer de nous faire plaisir, mais avec le « a » après le « 3 », c’est au‐dessus de ces capacités et il nous l’explique avec Unicode à l’appui :
$ perl6 -e 'say 1 + "3a"'
Cannot convert string to number: trailing characters after number in '3⏏a' (indicated by ⏏)
in block <unit> at -e line 1
Actually thrown at:
in block <unit> at -e line 1
TCL ne peut pas non plus, mais fait preuve d’un style plus stacktrace, en nous montrant petit à petit le code de la commande englobante :
$ cat main.tcl
puts [expr 1+{3a}]
$ tclsh8.5 main.tcl
can't use non-numeric string as operand of "+"
while executing
"expr 1+{3a}"
invoked from within
"puts [expr 1+{3a}]"
(file "main.tcl" line 1)
Lua 5.2 essaie aussi, mais n’y arrive pas. Un peu plus sérieux dans le ton :
$ lua52 -e 'print(1 + "3a")'
lua52: (command line):1: attempt to perform arithmetic on a string value
stack traceback:
(command line):1: in main chunk
[C]: in ?
Avec le Shell, c’est expéditif :
$ expr 1 + "3a"
expr: non-numeric argument
Ceux qui essaient de te comprendre
Perl 5 sent bien que c’est louche et te le fait savoir, mais se débrouille pour trouver 4 à la fin.
$ perl -wE 'say 1 + "3a"'
Argument "3a" isn't numeric in addition (+) at -e line 1.
4
AWK (BWK awk), trop fort, arrive à faire le calcul sans problèmes :
$ awk 'END{print 1 + "3a"}' /dev/null
4
JavaScript (node), rebelle, fait son original :
$ node -e 'console.log(1 + "3a")'
13a
C n’essaye pas vraiment de comprendre ce que tu voulais faire, mais ne veut pas trop te mettre la pression non plus :
$ cat main.c
#include <stdio.h>
int main(void) {
printf("%d", 1 + "3a");
return 0;
}
$ gcc -Wall main.c
main.c: In function 'main':
main.c:4: warning: format '%d' expects type 'int', but argument 2 has type 'char *'
$ clang -Wall main.c
main.c:4:15: warning: format specifies type 'int' but the argument has type 'char *' [-Wformat]
printf("%d", 1 + "3a");
~~ ^~~~~~~~
%s
1 warning generated.
$ ./a.out
289409602
Ceux qui te rejettent à la compilation
Go, ça parle simplement typage, mais il pointe le vilain du doigt :
$ cat main.go
package main
import "fmt"
func main() {
fmt.Println(1 + "3a")
}
$ go run main.go
# command-line-arguments
./main.go:6: cannot convert "3a" to type int
./main.go:6: invalid operation: 1 + "3a" (mismatched types int and string)
Avec OCaml, on parle typage, mais ça parle d’expressions, on sent l’esprit système de typage dans le style :
$ cat main.ml
let () = print_int (2 + "3a")
$ ocaml main.ml
File "main.ml", line 1, characters 24-28:
Error: This expression has type string but an expression was expected of type
int
Pour Haskell (à tryhaskell.org), c’est une question de manque d’instance pour une typeclass, sa façon de parler surcharge d’opérateur :
λ print (1 + "3a")
No instance for (Num [Char]) arising from a use of ‘+’
In the first argument of ‘print’, namely ‘(1 + "3a")’
In the expression: print (1 + "3a")
Rust parle traits, sa façon de parler surcharge, avec au passage quelques histoires de macros pour faire peur aux enfants. Et il nous dit qu’on peut avoir plus de détails en lui posant des questions au sujet d’E0277 (qui vaut le détour, ceci dit : un peu la même idée que perldiag, mais dans un style pédagogique).
$ cat main.rs
fn main() {
println!("{}", 1 + "3a");
}
$ rustc main.rs
main.rs:2:20: 2:28 error: the trait bound `_: std::ops::Add<&str>` is not satisfied [E0277]
main.rs:2 println!("{}", 1 + "3a");
^~~~~~~~
<std macros>:2:25: 2:56 note: in this expansion of format_args!
<std macros>:3:1: 3:54 note: in this expansion of print! (defined in <std macros>)
main.rs:2:5: 2:30 note: in this expansion of println! (defined in <std macros>)
main.rs:2:20: 2:28 help: run `rustc --explain E0277` to see a detailed explanation
main.rs:2:20: 2:28 help: the following implementations were found:
main.rs:2:20: 2:28 help: <f64 as std::ops::Add>
main.rs:2:20: 2:28 help: <&'a f64 as std::ops::Add<f64>>
main.rs:2:20: 2:28 help: <f64 as std::ops::Add<&'a f64>>
main.rs:2:20: 2:28 help: <&'b f64 as std::ops::Add<&'a f64>>
main.rs:2:20: 2:28 help: and 58 others
error: aborting due to previous error
Voilà, c’est tout.
P.-S. : Pour ceux qui recherchent des choses à lire plus dans l’esprit du jour, il y a cet article de chez TuxFamily que j’ai trouvé pas mal.
# D'autres
Posté par Benoît Sibaud (site web personnel) . Évalué à 10. Dernière modification le 01 avril 2017 à 14:33.
[^] # Re: D'autres
Posté par anaseto . Évalué à 4.
Haha, j'adore !
[^] # Re: D'autres
Posté par anaseto . Évalué à 3.
J'avais pas bash chez moi, donc je pouvais pas tester, et sur le moment j'avais en fait cru à un poisson :) Et puis non, c'est juste que t'avais oublié les guillemets (c'est censé être une erreur de syntaxe ^^). Du coup, j'ai découvert qu'on pouvait spécifier la base avec
$((1 + 2#11))qui renvoit4;)[^] # Re: D'autres
Posté par bunam . Évalué à 5. Dernière modification le 01 avril 2017 à 19:25.
-> 4
est bien plus simple
[^] # Re: D'autres
Posté par Anthony Jaguenaud . Évalué à 3.
Ton implémentation en c++, c’est ce que j’imaginais en C :
[^] # Commentaire supprimé
Posté par Anonyme . Évalué à 5.
Ce commentaire a été supprimé par l’équipe de modération.
# Elm rulez
Posté par Guillaume Denry (site web personnel) . Évalué à 10.
Voilà ce qui se passe quand on veut compiler une telle addition en Elm
Dieu que j'adore ce langage..
# En erlang
Posté par totof2000 . Évalué à 6.
Ca commence par raler à la compilation :
et à l'exécution:
# Question
Posté par Marotte ⛧ . Évalué à 8. Dernière modification le 01 avril 2017 à 21:13.
Est-ce qu’il existe un langage pour lequel la sortie serait : 59, de type entier donc ? (1 + 0x3A = 0x3B)
# Un peu déçu par Rust
Posté par Dring . Évalué à 5.
Rust est un langage qui m'attire vraiment beaucoup, mais par manque de temps je ne m'y suis pas encore mis. Jusqu'ici je n'ai vu que des belles choses, et le seul reproche que je lui trouvais, c'était la difficulté à trouver un librairie mature pour faire une application graphique.
Mais là, je trouve que le message d'erreur est… comment dire… Cryptique. Verbeux. Inutile. Décevant.
Curieusement, ça m'a décidé à enfin l'installer et commencer à m'amuser avec.
[^] # Re: Un peu déçu par Rust
Posté par Sufflope (site web personnel) . Évalué à 2.
Bonne chance avec les trois (!!) types de String dont je n'ai pas compris l'intérêt pour environ 1,5 d'entre eux.
[^] # Re: Un peu déçu par Rust
Posté par anaseto . Évalué à 3.
Rust n'est pas un langage très simple, mais il me semble (je suis juste un peu de loin le langage) qu'ils sont en train de faire des efforts pour le rendre plus accessible (dans la limite du possible avec un langage aussi ambitieux, bien sûr). En cherchant rapidement, je suis tombé sur un article Shape of errors…, donc peut-être que les messages d'erreurs sont plus amicals maintenant (ma version de rust doit dater de mi-2016).
[^] # Re: Un peu déçu par Rust
Posté par Shuba . Évalué à 5.
Avec un rustc plus récent:
Et le message d"erreur vient avec des couleurs qui rendent la lecture très agréable.
[^] # Re: Un peu déçu par Rust
Posté par Dinosaure (site web personnel) . Évalué à 2.
Rust est un langage typé au même titre que Haskell et OCaml. Il faut bien comprendre que les erreurs de types sont difficile à rendre compréhensible. La surcharge possible de l'opérateur
( + )en Rust complexifie la tâche et pour le coup, même si Haskell serait pour le coup un bonne exemple à suivre pour Rust, en général, c'est avec l'expérience qu'on comprends de manière évidente ces erreurs et on peut difficilement faire mieux.Tout ceux qui ont essayer de jouer avec les GADTs en OCaml savent de quoi je parle (
'a#0qui n'arrive pas à s'unifier avec'a#1) et que cette critique (pertinente) est à re-contextualiser par rapport à ce qu'on est capable de faire aujourd'hui et que la problématique reste encore difficile.Mais on peut aisément imaginer qu'avec l'engouement de reste, on est plus d'investissement humain pour résoudre ce problème.
[^] # Re: Un peu déçu par Rust
Posté par Marotte ⛧ . Évalué à 2.
Python permet la surcharge de l’opérateur
+(la fonction correspondante s’appelle__add__) et son message est on ne peut plus clair.En Haskell ça me semble un peu mieux mais c’est encore un peu « lourd », àmha.
Le message de Guile au contraire me plaît par sa concision.
C’est sûr que ça reste à mon avis une question de goût et comme tu le dis :
et une erreur de type c’est assez courant pour qu’on la reconnaisse du premier coup d’œil, même avec peu d’expérience. De manière générale on s’habitue à la tronche des messages. Du coup, même avec des messages d’erreur longs comme le bras, on sait tout de suite quelle ligne regarder.
Ça reste pénible quand on débute dans un langage.
[^] # Re: Un peu déçu par Rust
Posté par Dinosaure (site web personnel) . Évalué à 5.
Oui enfin Python n'a pas un algorithme d'unification derrière … Il faut comparer ce qui est comparable aussi (c'est pour ça que je compare pas cette problématique spécifique avec OCaml). Ce domaine demande encore pas mal de travail comme le prouve ce papier de recherche du OCaml Workshop 2014 notamment (si on prends la problématique dans sa globalité). Donc cette condescendance que Python y arrive mieux que Rust, non merci.
[^] # Re: Un peu déçu par Rust
Posté par Marotte ⛧ . Évalué à 2.
Désolé d’avoir pu paraître condescendent ce n’est que de l’ignorance de ma part, merci pour ta réponse.
[^] # Re: Un peu déçu par Rust
Posté par foobarbazz . Évalué à 2. Dernière modification le 03 avril 2017 à 09:33.
Après… Il y a un autre facteur qui rentre en compte, rust et haskell sont des langages jeunes, et qui s'adressent à une communauté de développeurs assez particulière, et que je ne saurais pas caractériser. Alors qu'à l'inverse, python est plus tout jeune, et qu'il s'adresse à tout un chacun.
À ce titre, un soin particulier à été apporté aux messages d'erreur de cpython. Alors que pour ghc (le compilateur haskell le plus utilisé) et l'implémentation de rust (dont j'ignore le nom), les messages d'erreurs sont très secondaires.
Et oui, détecter les problèmes de types c'est beaucoup plus difficile en haskell et en rust qu'en python. La raison c'est que les deux premiers les détecte au plus tôt, et python, au dernier moment. Dit autrement, haskell et rust vont analyser les raisons qui feront que le programme merdera, alors que python se contentera de détecter le merdage (c'est pas mal déjà).
[^] # Re: Un peu déçu par Rust
Posté par Guillaume Denry (site web personnel) . Évalué à 3.
Il me semble pourtant que Haskell et Python ont été créés à peu près la même année non ?
[^] # Re: Un peu déçu par Rust
Posté par Michaël (site web personnel) . Évalué à 6.
Hmm avec un première version datant de 1990 et une première implémentation du compilateur GHC datant de 1992, on peut certainement pas dire que Haskell est un langage aussi jeune que Rust.
Quelques dates, que j'ai recopiées de Wikipedia:
[^] # Re: Un peu déçu par Rust
Posté par Spack . Évalué à 10.
1995 a vraiment été une mauvaise année…
[ ]
[^] # Re: Un peu déçu par Rust
Posté par foobarbazz . Évalué à -3. Dernière modification le 03 avril 2017 à 13:50.
Oui, mais haskell c'était fils attardé de la fratrie, python permettait de faire des trucs de fous, alors qu'Haskell était toujours en mode « GNEEEEEEEEE "world!hello "… j'ai encore raté mon print :'( ».
Mais en fait, il était pas attardé, juste lent. 20 ans plus tard, python à l'air échappé des années 80 (80 c'est pour l'objet, si on enlève ça, c'est échappé les années 50) mais il sait bien s'habiller, il présente relativement bien, il a l'air moderne et "user friendly". Et Haskell est devenu l'un des langage les plus beaux qui soient.
[^] # Re: Un peu déçu par Rust
Posté par StyMaar . Évalué à 3.
Ce n'est pas pour autant impossible de faire un message clair: en pratique le message de Rust
contient exactement la même information que le message en Python :
À savoir qu'il n'y a pas d'opérateur défini pour l'opération entre un nombre et une string. On pourrait donc imaginer un message d'erreur dans ce style là :
[^] # Re: Un peu déçu par Rust
Posté par Michaël (site web personnel) . Évalué à 6.
Pas tout-à-fait quand-même, je vois deux différences importantes:
std::ops::Addalors que le programmeur a écrit+, alors que Python utilise le signe+.Le message de Rust est un peu plus difficile à comprendre il faut savoir (ou dans mon cas,deviner) que dans les message d'erreur:
le
_renvoie à la classe ou au type du bidule souligné, le1dans l'expression problématique et que le+est traduit en un appel à une méthodeAddlorsque cela est possible.Le message de Python se lit tout seul.
[^] # Re: Un peu déçu par Rust
Posté par StyMaar . Évalué à 3.
Cette phrase était en réponse à Dinosaure qui disait :
Mon argument était juste de dire que du point de vue de l'information disponible (pour le compilateur qui va générer le message) il n'y a rien qui manque en Rust qui lui permette de générer un message plus compréhensible.
Parce que clairement on est d'accord, le message en Rust est abscons tandis que le message Python est très clair.
[^] # Re: Un peu déçu par Rust
Posté par kantien . Évalué à 5.
Certes, mais même lorsque l'on fait du typage statique et que l'on utilise un algorithme d'unification, il est possible de renvoyer des messages plus compréhensibles. Le papier auquel tu renvoies donne des pistes, mais le message de Guillaume Denry sur elm est encore plus parlant. Elm a un système de type à la Haskell et son message d'erreur est on ne peut plus compréhensif et informatif.
Comme ces derniers temps je joue un peu avec Coq, qui doit faire face à des problématiques d'unification à coté desquelles celles de Rust sont un jeu d'enfant, je vais donner des exemples dans ce langage.
Pour commencer, il semblerait naturel de n'utiliser une notation infixe
x + yque dans une structure de monoïde. Alors je vais le faire façon type classes à la Haskell :Là on fait un type checking sur la fonction
monoid_op:Elle prend deux valeurs d'un certain type
?Aet renvoie une valeur de ce type, et cela dans un contexte où ce type est connu avec un monoïde sur les valeurs de ce type (le?signifie que le terme est indéterminé, la variable est existentielle : il existe une valeurAtelle que …). Si on lui demande de typer l'expression1 +' "3a", on obtient :Mais le plus amusant est qu'il peut typer le terme
"1" +' "3a"avant même de savoir le calculer :Maintenant pour lui permettre de calculer, on lui fournit une instance de la classe :
Pour le cas plus général où les deux opérandes ne sont pas du même type (et l'on se demande bien alors pourquoi utiliser la notation additive ?), et revenir à la situation de python, je vais l'illustrer ainsi.
Là on est dans la situation de python : comme il fait du typage dynamique, lors de l'appel au calcul de l'expression il vérifie si l'environnement permet de bien typer le terme (s'il peut instancier ces variables existentielles). Comme ce langage permet de modifier dynamiquement l'environnement, il est impossible de refuser statiquement ce code. Il pourrait, par exemple, être défini dans une bibliothèque où le code ne peut être évalué, puis importer dans un code qui rend l'évaluation possible. Comme dans le dialogue suivant avec la REPL Coq :
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Un peu déçu par Rust
Posté par Dinosaure (site web personnel) . Évalué à 1.
Une bonne occasion de me mettre au Coq (même si je continue à dire qu'il n'y a que les fous pour utiliser ce langage :p ).
[^] # Re: Un peu déçu par Rust
Posté par StyMaar . Évalué à 4.
Sinon, à mi-chemin entre Coq et des langages de programmation généralistes, tu as Idris. En plus il vient juste de sortir en version 1.0, ce qui stabilise pas mal de trucs.
[^] # Re: Un peu déçu par Rust
Posté par kantien . Évalué à 3.
J'ai regardé un peu la documentation de Idris et je ne suis pas convaincu que cela simplifie les choses par rapport à Coq.
Une des fonctionnalité centrale des langages avec types dépendants (les types sont des citoyens de première classe, comme les fonctions le sont dans les langages fonctionnels) est de pouvoir prouver des théorèmes de spécification et de correction sur les programmes. Or quand je lis les deux exemples de la documentation : l'addition est associative sur les entiers et l'addition est commutative, je ne trouve pas cela plus simple. Il faut écrire un module dans un fichier avec une preuve laissée indéterminée, chargé le module dans la REPL, utiliser les tactiques pour effectuer la preuve puis recopier le script de preuve dans le fichier.
Avec CoqIde, pour la preuve d'associativité j'écris cela dans un fichier :
Les preuves en Coq ou Idris peuvent se paraphraser ainsi :
On prouve le théorème par récurrence sur l'entier
n.n = 0alors après simplification il faut prouver quem + p = m + pce qui est trivial.n = S n'alors il faut montrerS n' + m + p = S n' + (m + p), ce qui revient, par définition de la fonctionplus, à montrer queS (n' + m + p) = S (n' + (m + p))(c'est là l'appel à la tactiquesimplqui effectue des réductions de calcul à partir de la définition deplus). Or, d'après l'hypothèse de récurrence on an' + m + p = n' + (m + p), il suffit donc de montrerS (n' + (m + p)) = S (n' + (m + p))(là c'est la sérieintros. rewrite IHn) ce qui est trivial.Avec un peu de pratique, on peut factoriser les parties communes entres les deux cas de la preuve par récurrence est aboutir à cette preuve :
Les preuves se construisent pas à pas comme décrit dans la documentation de Idris et elles ne semblent pas plus compliquées à effectuer. Je dirais même que vu l'éventail de tactiques disponibles de base avec Coq, elle sont même sans doute plus simple. Exemple :
Ensuite, il y a un point qui me chagrine dans l'article de présentation de Edwin Brady. Au paragraphe 3.5 page 14, il écrit :
Ici c'est moi qui graisse, parce que pour le Calcul des Constructions Inductives (qui est à Coq ce que TT est à Idris) on n'en est pas au stade de la conjecture mais d'un résultat établi. Est-ce bien une conjecture pour TT ou le résultat a été prouvé ?
De plus, même si je peux comprendre le choix fait pour contrôler si les fonctions définies sont totales ou partielles (paragraphe 3.6), il est plus strict que celui de Coq qui permet de définir des fonctions totales qui seront considérées (à tort) comme partielles par Idris (d'un autre côté en Coq il n'y a pas le choix : les fonctions sont toutes totales).
Pour apprendre en douceur et progressivement la programmation en Coq lorsque l'on vient de la programmation fonctionnelle sans type dépendant (Haskell ou OCaml, par exemple), à mon avis le plus simple est de lire le livre (en anglais) Software Foundations de Benjamin C. Pierce disponible en ligne avec le code associé. D'ailleurs le livre est écrit en Coq et la version htlm est générée via l'utilitaire
coqdoc.Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Un peu déçu par Rust
Posté par Michaël (site web personnel) . Évalué à 5. Dernière modification le 03 avril 2017 à 12:18.
Si on sort des exemples bétas
1 + "two"et bien non les erreurs de type ne sont pas faciles à repérer à la lecture. Ces temps-cis je travaille sur un code NodeJS qui lit depuis une base de données. La BDD a des capacités de tri limitées et l'API que j'implémente doit aussi proposer du tri et de la réduction de données (un peu comme legroup byde SQL pour faire vite). Dans le code existant, la lecture de la BDD produit un flot d'items, mais pour pouvoir profiter des capacités de tri de celle-ci, j'ai décidé de changer en un “flot de pages d'items peut-être triées” ce qui simplifie beaucoup la communication entre les modules de l'application. Un langage comme OCaml ou Haskell permet au compilateur de détecter automatiquement toutes les zones de code affectées par ce changement de type. JavaScript ou les langages typés dynamiquement en général n'apportent simplement aucune aide pour résoudre ce problème – qui est pourtant le pain quotidien du programmeur non?Autre exemple plus béta, on ne reconnaît pas forcément du premier coup d'œil qu'il fallait écrire
if("names" in params)plutôt queif(names in params)et le compilateur d'un langage typé statiquement détecte l'erreur instantanément. Dans mon application NodeJS avec du code asynchrone, je me retrouve avec une exception et une pile d'erreur inutilisable car toutes les fonctions référencées sont des callbacks d'une bibliothèque pour la programmation asynchrone et donc pas du code utilisateur.Je n'ai donc aucun mal a percevoir l'intérêt du typage statique.
[^] # Re: Un peu déçu par Rust
Posté par StyMaar . Évalué à 2.
Si tu veux du typage statique en Node (ou JavaScript en général), tu peux utiliser flow: tu rajoutes juste des annotations de type à ton JavaScript et un compilateur (écrit en OCaml) va vérifier que ton typage est correcte. Il est même capable de faire un peu d'inférence de type (mais pas dans tous les cas je crois). Le système de type est assez complet, avec des génériques, des types sommes et des objets non-nullables par défaut. Ce qui est bien c'est que ton code reste du JavaScript, contrairement a TypeScript, qui t'oblige à changer ton utilisation du langage.
[^] # Re: Un peu déçu par Rust
Posté par Michaël (site web personnel) . Évalué à 3.
J'ai entendu parler de flow mais je ne l'ai jamais encore essayé. Je n'en attends pas grand chose, en Javascript il y a beaucoup d'obstacles qui empêchent le système d'être très pertinent, et j'avais discuté avec un des développeurs du projet qui avait présenté flow à React en 2016 (à Paris) qui avait plus ou moins confirmé mes craintes. L'idée d'annoter les types me semble vider un peu le concept de son intérêt puisque si justement les types étaient notés explicitement on pourrait retrouver relativement facilement les endroits affectés par un changement de type – même si un système automatique peut sûrement apporter son aide. Mais j'essaierai quand-même de voir ce que ça donne.
Je rappelle pour ceux qui lisent que OCaml ou Haskell déduisent les types et vérifient leur cohérence sans aucune annotation de l'utilisateur. En pratique on écrit souvent ces types déduits dans un fichier, mais le système est capable de générer un canvas qu'il suffit de compléter.
[^] # Re: Un peu déçu par Rust
Posté par StyMaar . Évalué à 1.
Ils peuvent le faire, mais (dans la communauté Haskell du moins) il est généralement recommandé de mettre des annotations de type au niveau des fonctions, dans un but de documentation du code et pour expliciter les invariants, même si le compilateur serait capable de s'en passer.
Par exemple :
http://learnyouahaskell.com/types-and-typeclasses
Qu'on peut traduire par : En écrivant nos propres fonctions, on peut choisir de déclarer explicitement leur type. C'est généralement considéré comme une bonne pratique, sauf dans le cas de fonctions très courtes.
[^] # Re: Un peu déçu par Rust
Posté par Michaël (site web personnel) . Évalué à 2.
C'était la phrase “mais en pratique…” du commentaire auquel tu réponds ;)
[^] # Re: Un peu déçu par Rust
Posté par foobarbazz . Évalué à 1.
OCaml sait faire ça, pas Haskell :
Le compilo répond :
En précisant le type de undefined ça marche.
[^] # Re: Un peu déçu par Rust
Posté par Anthony Jaguenaud . Évalué à 2.
En même temps, undefined pouvant se faire passer pour n’importe lequel, quel critère proposes-tu pour que le compilateur détermine le bon type à la compilation ?
[^] # Re: Un peu déçu par Rust
Posté par foobarbazz . Évalué à 3.
C'était pas pour critiquer Haskell, c'était juste pour pour souligner cette différence entre Haskell et OCaml.
Le fait est que le système de type de Haskell est beaucoup plus puissant que celui d'OCaml, et ce n'est pas gratuit…
Le problème en l’occurrence ne vient pas de l'existence du "undefined" d'haskell, je m'en suis servi ici pour simplifier l'exemple. J'aurais pu écrire :
En fait, un programme aussi simple que :
Soulève le problème. "1" a un type polymorphe :
Num t => t, autrement dit, est que c'est un Int, un Integer ? un Float, un Rational ? Un entier de peano défini par l'utilisateur ? Bon, le compilo n'est pas si chiant, il compile quand même, mais avec les warning il précise quand même qu'il "Defaulting the following constraints to type ‘Integer’"Il y a un mécanisme de résolution par défaut dont je ne connais pas le fonctionnement.
[^] # Re: Un peu déçu par Rust
Posté par octachron . Évalué à 2. Dernière modification le 04 avril 2017 à 20:13.
Ce n'est pas vraiment une différence entre OCaml et Haskell, en OCaml aussi les usages avancés du système de type requièrent des annotations de type explicite: que ce soit au niveau des modules et foncteurs, des types algébriques généralisés, du polymorphisme de second ordre, ou de la récursion polymorphique.
Il est peut être plus courant de se heurter à ces problèmes en Haskell, mais le problème sous-jacent reste le même: au-delà d'un certain niveau d'expressivité du système de type, l'inférence devient indécidable, et le compilateur a besoin que le programmeur explicite son intention.
[^] # Re: Un peu déçu par Rust
Posté par foobarbazz . Évalué à 1.
Tu as un exemple de programme qui compile pas sans annotation ?
Je connais beaucoup mieux Haskell que OCaml.
[^] # Re: Un peu déçu par Rust
Posté par octachron . Évalué à 3.
Au niveau du système de module, des annotations de types sont nécessaires pour les arguments des foncteurs:
Les modules récursifs eux ont besoin d'être totalement annoté, par exemple:
Ce besoin d'annotation pour les modules peut se propager dans les fonctions à cause
des modules locaux (ou de première classe).
Un autre cas classique d'annotation explicite apparaît pour la récursion polymorphique
sur les types récursifs non homogènes:
Dans ce cas, l'annotation
'a.'a arbre_complet -> intqui équivaut àforall 'a.…est nécessaire car le type du paramètre
'aà l'intérieur de la définition dehauteuret à l'extérieur diffère.Pour le polymorphisme de second ordre, OCaml ne supporte pas directement les annotations
forallà l'intérieur des arguments de fonctions, il faut donc passer soit par des types enregistrements(records):ce qui est plus contraignant qu'une annotation directe, soit par le système objet
Sans cette annotation le typeur va essayer d'unifier le type de
1et[]et renvoyer une erreur.Les GADTs de leur côté sont toujours lourds en annotations en Haskell ou OCaml
Enfin, une particularité d'OCaml du aux effets de bords, ce sont les types faiblement polymorphiques, qui ne peuvent pas être exporté par une unité de compilation, ce qui peut nécessiter d'ajouter des annotations de type pour les éliminer. Par exemple, un fichier
a.mlne compile pas sans son annotation de type.
# Re : Journal Un print(1 + "3a"), ça nous inspire comment ?
Posté par harlock974 . Évalué à 5.
En résumé : il existe beaucoup trop de langages de programmation…
[^] # Re: Re : Journal Un print(1 + "3a"), ça nous inspire comment ?
Posté par Sacha Trémoureux (site web personnel) . Évalué à 8.
T'as raison, il faudrait un standard unique pour les unir tous.
Qui s'y met ?
[^] # Re: Re : Journal Un print(1 + "3a"), ça nous inspire comment ?
Posté par Sufflope (site web personnel) . Évalué à 3.
ColdFusion.
https://cfdocs.org/createobject
# Merci
Posté par Christophe G. . Évalué à 2.
Merci anaseto pour cette grosse tranche de rigolade au réveil !
Ça me confirme dans mon idée que j'aime vraiment, vraiment beaucoup les messages d'erreur de Clang.
Fais-moi plaisir, apporte-moi une clope, un whisky et toi. -- Matmatah
# Let's talk about JavaScript
Posté par ohm . Évalué à 8.
https://www.destroyallsoftware.com/talks/wat
# R
Posté par Le Pnume . Évalué à 4.
Error in 1 + "3a" : argument non numérique pour un opérateur binaire
# Java
Posté par Spack . Évalué à 8.
Personne pour du Java ?
[^] # Re: Java
Posté par totof2000 . Évalué à 2.
On parle de langage, pas de bloatware.
[^] # Re: Java
Posté par Marotte ⛧ . Évalué à 2.
C’est marrant je viens de faire le test juste avant de lire ton message parce que j’avais en tête des messages d’erreur à l’exécution valant le détour en Java… mais non, ça marche.
Comme Javascript ça "cast" silencieusement vers string, c’est sûr que si on (int,str) alors qu’on attend soit (int,int) soit (str,str), choisir le deuxième, donc faire un int → str c’est être sûr que ça va fonctionner :)
[^] # Re: Java
Posté par Axioplase ıɥs∀ (site web personnel) . Évalué à 6.
Ca "cast" pas, ca appelle toString().
[^] # Re: Java
Posté par ckyl . Évalué à 2.
Pour être exacte ça s'appelle String Concatenation Operator +.
[^] # Re: Java
Posté par xcomcmdr . Évalué à 3.
le grand cousin C# avec la console "C# interactive" de Visual Studio 2015 :
Pas drôle.. :(
"Quand certains râlent contre systemd, d'autres s'attaquent aux vrais problèmes." (merci Sinma !)
[^] # Re: Java
Posté par TImaniac (site web personnel) . Évalué à 3.
C'est assez largement utilisé en C#, le + est l'opérateur de concaténation de chaîne et la classe de base Object a un opérateur ToString : ca fonctionnera donc toujours.
# SBCL
Posté par ylsul . Évalué à 6.
SBCL a été assez clair : il indique que "3a" n'est pas un nombre.
Après il affiche la pile d'appels, c'est souvent utile quand un programme plante. Par contre la pile n'est pas des plus claires, surtout que sur un petit exemple comme ça elle contient plus de machinerie de SBCL que de fonctions du développeur. On voit quand même qu'elle contient les valeurs des paramètres passés aux fonctions (trame 9 notamment), ce qui est parfois utile.
Sinon j'avais lu des éloges sur Elm et ses messages d'erreur, joli…
# Eiffel
Posté par Philip Marlowe . Évalué à 2.
Error code: VWOE
Error: invalid Operator_expression.
What to do: make sure that equivalent dot form is valid Call.
Class: APPLICATION
Feature: make
Formal type: INTEGER_32
Actual type: attached STRING_8
Line: 21
--| Add your code here
-> print (1 + "3a")
end
# En Scala
Posté par picman . Évalué à 2.
Le Scala élève le type du Integer vers Any et peux les concaténer via :
[^] # Re: En Scala
Posté par Sufflope (site web personnel) . Évalué à 2.
C'est pas tout à fait ça, toute classe hérite de Any en Scala, et ce code est l'ancienne version et il manque la méthode implicite de conversion qui allait avec :
Maintenant ça utilise les implicit class (qui datent de 2.10 je crois ?) pour tout faire en une fois dans Predef :
Y a rien de magique, ce qu'il se passe c'est que le compilateur scala cherche la méthode +(other: String) sur Int, ne la trouve évidemment pas, alors il cherche (entre autres ; pour l'ancienne version il cherchait une méthode implicite prenant en unique paramètre un truc permettant de passer des Int, et ayant pour type de retour un truc ayant une méthode +(other: String)) une classe qui soit implicite, à un seul paramètre de constructeur (de type permettant de passer un Int, ce qu'est Any puisque tout objet est un Any), et disposant d'une méthode +(other: String), ce que any2stringadd est.
Donc il remplace ton 1 + "3a" par :
Et (rien à voir avec ce qui permet de concaténer des carottes et des String, c'est orthogonal) le extends AnyVal fait de any2stringadd une value class, c'est à dire une classe wrapper que le compilo est encouragé à virer dans le code final. Donc là en l'occurence ce qui arrive à la fin c'est que + est "inlinée" et ça donne au final :
# Le but ?
Posté par TilK . Évalué à 6.
Salut,
J'ai du mal à comprendre ce que tu essaies de montrer/calculer.
Il y a d'abord pour moi les langages dans le "+" n'est que l'opérateur d'addition des nombres. Ceux là, doivent renvoyer une erreur de type : Shell, Php, Perl, Elm…
Il y a certains langages dont le "+" est la fois l'opérateur d'addition des nombres et l'opérateur de concaténation des chaînes de caractères.
Parmi ceux là, il y a ceux qui se basent seulement sur le type de l'opérande de gauche pour savoir s'il faut réaliser une addition ou une concaténation.
Ceux-là doivent normalement lever une erreur : Ruby, Python…
Ceux qui sont regardent le type des deux opérandes pour savoir s'il faut réaliser une addition ou une concaténation et qui sont capable de faire du trans-typage doivent renvoyer la chaîne "13a" : Java, Javascript, Scala…
Et puis, il y a le C, qui utilise le "+" comme opérateur d'addition de pointeur avec un nombre, et il sort une réponse presque logique : "a".
Donc en gros, si j'ai tout bien compris, tu montres qu'il faut connaître la syntaxe et la grammaire d'un langage pour l'utiliser,et qu'il y a des mauvais élèves pour expliquer ou montrer une erreur, c'est bien cela ?
Si tu voulais comparer les messages d'erreur, n'aurait-il pas mieux utiliser un opérateur possédant moins de signification ? Par exemple "/" ou "*" ?
[^] # Re: Le but ?
Posté par anaseto . Évalué à 9.
Eh bien, faut pas chercher un truc très profond. Ce qui est intéressant, c'est qu'observer la réaction d'un langage sur cette simple opération en dit pas mal sur ses particularités : typage statique ou non, typage fort ou faible (tous vs C/C++), style objet, système de type à la fonctionnelle ou typage plus simple (par exemple Ruby vs Haskell vs Go), surcharche d'opérateur ou non, opérateur qui coercitionne les arguments en fonction de la valeur de retour ou choisit la valeur de retour en fonction de ceux-ci (Perl vs Javascript), qui essaye de deviner ou non (
"3a"vs"3") (awk vs lua), stacktrace par défaut ou non (sbcl vs guile), messages d'erreurs pensés pour débutants ou connaisseurs, etc.[^] # Re: Le but ?
Posté par gouttegd . Évalué à 7.
Euh, non, dans l’exemple donné le programme C sort une valeur qui, sauf erreur de ma part, devrait être l’adresse de la chaîne "3a" incrémentée de 1.
Ce qui correspond à ce qui est attendu d’après le standard C (section 6.5.6, §4 : When an expression that has integer type is added to or subtracted from a pointer, the result has the type of the pointer operand).
D’ailleurs, l’avertissement du compilateur (aussi bien gcc que clang) ne concerne pas le fait d’additionner un entier et un pointeur (il n’y a pas lieu d’avertir de quoi que ce soit puisque c’est quelque chose de prévu par le standard), mais la discordance entre le type attendu d’après la chaîne de format ("%d", soit un entier) et le type de l’expression correspondante (pointeur, conformément à la règle sus-citée). Un appel de la forme
printf("%p", 1 + "3a")ne provoque aucun avertissement.[^] # Re: Le but ?
Posté par Anthony Jaguenaud . Évalué à 4. Dernière modification le 03 avril 2017 à 15:42.
Ben si, c’est exactement ce qu’il dit :
Et puis, il y a le C, qui utilise le "+" comme opérateur d'addition de pointeur ("3a") avec un nombre (1), et il sort une réponse presque logique : "a" (quand on met printf(1+"3a") et non la version avec "%d").
Je ne l’avais pas vu ambigüe.
[^] # Re: Le but ?
Posté par Jean Parpaillon (site web personnel) . Évalué à 3.
Le but ? Pour moi c'est très intéressant: la prochaine fois que je dois choisir un langage, ça donne des informations très importantes.
Personnellement, le langage qui ne râle pas et qui "essaye de deviner" pour toi, je l'élimine de suite. Mais ça, c'est mes critères… Enfin, j'ai mes raisons:
Imaginons:
FONCTION (a)
SI a > 100 ALORS
DECLENCHER GUERRE NUCLEAIRE…
SINON
CA VA…
FIN SI
FIN
Et maintenant, imaginons que 'a' vienne de l'addition de cet article: j'aimerais bien être sûr que le résultat de l'addition soit prévisible et pas interprétée avec une foultitude de règles genre javascript: si le deuxième argument peut-être casté vers une string, je caste le premier sauf si il ressemble à un int (c'est quoi, "ressembler à un int" ?). Enfin bref, revoir le lien déjà posté:
https://www.destroyallsoftware.com/talks/wat
"Liberté, Sécurité et Responsabilité sont les trois pointes d'un impossible triangle" Isabelle Autissier
[^] # Re: Le but ?
Posté par Christophe B. (site web personnel) . Évalué à 3.
J'ai lu quelque part que l'on peut juger du niveau d'un logiciel en fonction des erreurs qu'il est capable de gérer …
il est bien loin le temps des "syntax error" génériques qui pouvait rendre fou :)
pour ma part je préfère de loin des langages qui "t'aide à la correction" comme python plutôt que des langages laxistes comme php.
D'un autre coté si vous aimez la rigueur pure et dure … il y a ada … mais pour avoir testé c'est un peu too much …
[^] # Re: Le but ?
Posté par Christophe B. (site web personnel) . Évalué à 4.
D'ailleurs en Ada cela ne compile pas …
[^] # Re: Le but ?
Posté par Blackknight (site web personnel, Mastodon) . Évalué à 3.
En même temps, tu fais pas d'effort ;)
Il faut juste lui dire comment faire :)
Par contre, c'est pas commutatif, il faudrait aussi écrire ce que l'on fait dans l'autre sens.
[^] # Re: Le but ?
Posté par Christophe B. (site web personnel) . Évalué à 4.
OK pris en flag …
cela m'apprendra à la ramener sur un langage que j'ai survolé (mais que j'ai beaucoup apprécié et déplore le manque de temps pour réellement le pratiquer)
Ada en demande beaucoup, mais en retour si la compilation passe c'est que déjà beaucoup de choses ont correcte
Est ce vrai ou je me trompe lourdement ?
[^] # Re: Le but ?
Posté par Blackknight (site web personnel, Mastodon) . Évalué à 2. Dernière modification le 04 avril 2017 à 12:10.
Globalement, c'est vrai mais ça ne corrige pas les erreurs d'algo qui déclenchent des exceptions ;)
Ceci dit, il y a aussi des cas où ça peut se planter alors que ça compilait très bien.
Typiquement, je pense à l'utilisation des bindings.
La majeure partie du temps, ce sont des bibliothèques C/C++ qui sont liées et du coup, elles introduisent l'utilisation de pointeurs venant directement du code C et là, c'est le drame ;)
Ada n'est pas la panacée mais c'est vrai qu'une fois que j'ai corrigé toutes les erreurs de compilation, je suis déjà plus sûr de mon coup :D
Enfin, cela ne représente que mon avis…
[^] # Re: Le but ?
Posté par Christophe B. (site web personnel) . Évalué à 2.
Non bien sur, mais j'avais été surpris par les 'missing case values:' et avais trouvé cela très bien, cette obligation de mettre un cas par défaut quand on utilise un case par exemple.
En revanche la courbe d'apprentissage est plutôt rude … dommage
[^] # Re: Le but ?
Posté par Blackknight (site web personnel, Mastodon) . Évalué à 1.
Il faut y aller petit à petit et ne pas chercher à manipuler le langage dans son ensemble d'un seul coup.
Personnellement, il y a encore un tétra chiée de trucs dans la norme que je n'ai pas encore utilisés ;)
[^] # Re: Le but ?
Posté par Sufflope (site web personnel) . Évalué à 3.
Mouais ça n'a pas grand chose à voir avec (pour le meilleur et pour le pire) les langages où on peut ajouter des choux et des carottes. C'est sûr que si tu écris une fonction permettant explicitement et seulement d'additionner des Int et des String, le programme va pouvoir additionner des Int et des String, encore heureux.
[^] # Re: Le but ?
Posté par Blackknight (site web personnel, Mastodon) . Évalué à 2.
Ce que je voulais dire c'est que comme rien n'est implicite, il faut écrire la fonction pour l'autre addition et ainsi assurer la commutativité de l'addition, ce qui n'a rien d'obligatoire…
La version exhaustive serait, du coup, celle-là
Certes mais je préfère dire ce que je veux faire que d'avoir un comportement inféré qui n'est pas forcément vrai… Bien qu'à partir du moment où on écrit '+', il semble, par convention, obligatoire que l'opération soit commutative.
[^] # Re: Le but ?
Posté par Michaël (site web personnel) . Évalué à 2.
Je n'ai encore jamais essayé mais il semblerait que PHP 7.0 implémente un typage statique (optionnel). Quelqu'un a une expérience avec ça?
# Et en brainfuck ?
Posté par Philippe F (site web personnel) . Évalué à 4.
Je suis déçu, le brainfuck ne permet pas de faire ce genre d'opération complexe. J'aurai été curieux de voir le message d'erreur…
[^] # Re: Et en brainfuck ?
Posté par benji39 . Évalué à 0.
Il aurait peut-être répondre "4a" ! Comme aucun autre langage apparemment, pas si compliqué pourtant.
# Le langage ou le compilateur/interpréteur ?
Posté par mahikeulbody . Évalué à 1.
Le comportement (i.e. choix effectué face à la situation) et l'affichage du comportement (i.e. le message d'erreur ou le warning généré) sont-ils intrinsèques au langage (i.e. décrit dans sa définition) ou bien juste au compilateur/interpréteur ?
Y a t-il des langages ayant plusieurs compilateurs/interpréteurs ? Si oui, il faudrait distinguer les cas où le comportement obtenu est décrit par le langage ou bien résulte du "complément de définition" apporté par le compilateur…
Un langage dont le comportement* est défini par sa définition ET son compilateur est-il un bon langage ?
* J'admets que l'affichage du comportement puisse relever du seul compilateur.
[^] # Re: Le langage ou le compilateur/interpréteur ?
Posté par anaseto . Évalué à 3.
En l'occurrence, je pense qu'ici, dans tous les cas, le comportement est bien défini par tous les langages du fil (par exemple si awk renvoit 4 c'est parce qu'il utilise la fonction de la libc standard
strtodpour produire un nombre à partir d'une chaîne, c'est documenté dans le manuel). Le message d'erreur et son style par contre peuvent dépendre dans une plus ou moins grande mesure du compilateur (par exemple gcc vs clang pour le C/C++).Suivre le flux des commentaires
Note : les commentaires appartiennent à celles et ceux qui les ont postés. Nous n’en sommes pas responsables.