Guillaum a écrit 472 commentaires

Idris2 est une sorte d'Haskell en plus poussé. La version 2 s'appuie sur la « Quantitative Type Theory ». Ça permet d'écrire des mettre des nombres dans les types, comme …
Je n'ai pas vraiment réussi à comprendre ce que ça apportait en pratique pour les développeurs. Et je n'ai pas été spécialement été attiré par ce que j'ai vu. C'est probablement très intéressant, mais je ne dois pas être la bonne personne pour ça.

"Ecrire des nombres dans les types" ce n'est pas nouveau, cela se fait depuis des années dans de nombreux langages. C++ par exemple te permet d'avoir des nombres au niveau du type. Haskell fait cela très bien aussi. Idris apporte cependant plus de confort sur des cas plus avancés, que je ne détaillerais pas ici.

Ecrire des nombres dans des types peut permettre de rendre des interfaces plus robustes avec des vérifications à la compilation. L'exemple canon c'est celui des vecteurs que tu as donné, qui permet par exemple d’empêcher (à la compilation) les accès à des cases qui n'existe pas. Un autre exemple serait la multiplication de matrice : celle-ci ne fonctionne normalement qu'avec des matrices ayant des tailles en correspondance. En gros, multiplier une matrice de taille "N * M" avec une matrice de taille "N' * M'" donne une matrice de taille "N * M'". À partir du moment ou tu es sensibilisé à ce type de pratique, tu commences à voir des cas d'application partout. En réseau, tu peux imaginer avoir un tag dans ton type de socket pour connaitre son état actuel, et ainsi empêcher des cas impossibles. Tu peux imaginer ajouter l'unité d'une grandeur physique afin de refuser d'ajouter des mètres et des grammes. Tu peux imaginer une librairie de gestion de chemin de fichier qui sait (à la compilation) si le chemin est absolu ou relatif. Une librairie de gestion de couleur qui n’autorise que les traitements dans des espaces colorimétriques compatibles. Une librairie de géométrie qui interdit des opérations mal définie (addition de deux positions. Translation d'une position en deux dimension par un vecteur 3 dimensions). Si tu as une libraire de dessin (type cairo) avec plusieurs backend supportant chacun différentes fonctionnalités, tu peux imaginer que le type final de ton dessin "liste" les fonctionnalités nécessaires et refuse (à la compilation) de générer une sortie si le backend n'en est pas capable. Si tu fais du web, tu peux imaginer un langage au dessus de CSS / HTML qui s'assure (à la compilation) que tu n'a pas d'incohérence dans les noms de tes classes CSS. Tu peux aussi vérifier (à la compilation) que tous tes liens internes de ton site web pointent vers des ressources qui existent.

La liste est infinie, le but est encore une fois d’empêcher de compiler des programmes qui ne sont pas correctes. Tout ce que tu peux exprimer au niveau du type c'est des erreurs en moins à l’exécution et des tests en moins à faire. C'est un compromis à évaluer en fonction de trop nombreux paramètres : comme ton aisance avec le langage, la simplicité de celui-ci, l'impact sur le temps de développement, l'impact d'une erreur runtime en production, l'impact sur l'évolution future du code. Ce n'est pas facile à évaluer ;)

C'est une déclaration de variable, comme int riguant.

Je dirais que la partie gauche accepte les parenthèses pour permettre de grouper les choses, comme par exemple entre int *(foo[]) versus int (*foo)[]).

En C (et C++), on peut voir la déclaration de type comme deux parties. La gauche, le type primitif, et la droite, comme "une expression qui permet d’accéder à ce type".

Par exemple, int *p; signifie que *p permet d’accéder à un int. Donc p est un pointeur.

En partant de là, si les parenthèses sont autorisées, pas de raison de les interdire dans le cas ou l'expression se réduit à un nom.

Je ne suis pas expert du domaine et c'est avec plaisir que je me ferais contredire. Mais j'ai l'impression que cette solution est vouée à l'échec car tu aura toujours sur la machine un moyen de lancer quelque chose d'une manière ou d'une autre. Est ce que /tmp sera aussi en noexec ?

J'ai l'impression que si tu veux ce type d'encapsulation c'est un autre outil qu'il te faut. Type docker ou autre.

Ceci étant dit, tu peux toujours:

a) interdire à ton utilisateur d'utiliser nix (le démon peut filtrer les requêtes d'installation basé sur le userid.
b) Le monter dans un file système virtuel qui ne montre que les chemins autorisés. (Cela revient à virtualiser).

Bref. J'ai l'impression que la sécurité dans ce contexte est plus complexe que juste "interdire d'installer n'importe quoi".

J'ai toujours trouvé que cet argument était un faux argument. Le pirate pourra toujours installer les packages localement dans son répertoire. C'est sans doute un poil plus de travail que nix-shell -p gcc -p gdb, mais c'est à la portée de tout pirate qui se respecte.

Hello !

En effet. Merci. Je suis donc moins triste ;)

Parce que PyF https://github.com/guibou/PyF, une librairie Haskell qui implémente l'équivalent des f string de python (parce que c'est tellement bien en python qu'il me fallait la même chose en Haskell), ne souffre pas de ce bug, car je n'ai jamais été capable d’implémenter la récursion dans les paramètres de remplacement.

L'adoption du langage m'importe peu, surtout si pour des raisons que je considère futiles. C'est le même débat que l'indentation significative en python ;)

Personnellement je trouve que cette syntaxe a -> b -> c représente bien mieux les deux possibilités f(a) -> (b -> c) ou f(a, b) -> c qu'une autre syntaxe et je trouve que c'est une très bonne manière de faire comprendre ce concept et d'amener à l'utilisation d'application partielle. Mais au final on s'en fout ;)

la vérification que l'appel a le bon nombre d'argument est retardée.

J'ai déjà avoué dans un autre commentaire que cela pouvait générer des erreurs de type parfois étonnantes, mais je répète que dans mon expérience cela ne m'a jamais dérangé. Cependant mon expérience se limite à Haskell et donc j'ai du mal à voir ce que cela peut donner dans un autre langage.

la lisibilité si tu as fn f: a b -> c, tu vois tout de suite que tu a et b comme entrée et c comme retour, si tu as fn f: a -> b -> c, c'est moins immédiat.

L'application partielle biaise notre façon de développer des interfaces, on s'habitue très vite à voir f comme plusieurs possibilités, celle qui te semble immédiate (2 arguments, un retour qui n'est pas une fonction), et l'autre (un argument, un retour qui est une fonction).

Après si vraiment tout cela t’embêtes et que c'est la seule chose qui te bloque en Haskell, tu peux faire des fonctions qui prennent des tuples, ainsi fn aura comme type (a, b) -> c et son appel se fera avec un tuple: fn (a, b). La vérification sera faite "au bon endroit", la syntaxe de déclaration de fonction va ressembler à quelque chose que tu connais et tout sera bien et chaque fois que tu auras besoin d'une fonction appliquée partiellement, tu pourras faire une lambda: \x -> fn(a, x) ;)

Ma citation était mauvaise, je voulais troller sur les fonctions avec un nombre variable d'argument.

Tu disais:

Par contre pour pouvoir gérer les fonctions avec un nombre variable d'éléments,

C'est sur cela que je répondais, pardon. Gérer des fonctions avec un nombre variable d'argument, je ne suis pas forcement fan.

Je n'ai rien contre ta proposition de f(x, _, z) représentant la création d'une fonction anonyme y -> f(x, y, z). J'avoue que je ne sais pas vraiment si c'est mieux ou moins bien et que je suis habitué à la version Haskell. On pourrait surement faire une comparaison poussée des différences entre les deux syntaxe, à un moment il faut faire un choix.

Par contre pour pouvoir gérer les fonctions avec un nombre variable d'éléments, j'aime bien l'idée d'une opérateur .. ou _* pour remplacer un ou plusieurs éléments a la fin.

Pour troller je te répondrais bien "sympa comme fonctionnalités mais par défaut pas OK". Cela peut générer son lot de bugs amusants aussi. En fait je n'ai jamais trop vu intérêt de cette fonctionnalité (et même après des décennies de python ;)

1) Les arguments nommés et ou à valeur par défaut me manquent terriblement en Haskell donc je suis d'accord avec toi ;)

2) Ce ne sera pas un bug mais une erreur de type. Certes pas forcément toujours évidente et pouvant se propager un peu plus loin à cause de l'inférence de type. En pratique c'est rarement un problème dans mon expérience.

Je m'auto répound pour ajouter un truc. La déclaration de fonction en Haskell fait du "pattern matching" en même temps. La plupart du temps on ne pas pas utiliser des variables "simples", mais un "pattern".

Exemple, pour faire une somme (il y a plus simple pour faire une somme, comme la fonction sum, c'est juste pour l'exemple).

mySum :: [Int] -> Int
mySum [] = 0
mySum (x:xs) = x + mySum xs
Ici on commence par le type [Int] -> Int. Puis vient l'implementation. Premier cas, la somme d'une liste vide [] qui vaut 0. Second cas, la somme d'une liste qui contient un élément x et une suite de liste xs.

En utilisant la syntaxe "go", c'est à dire ou les variables ont leur type directement collé, cela donnerait un truc du genre:

mySum ([] :: [Int]) = 0
mySum (((x :: Int) : (xs :: [Int])) :: [Int]) = x + mySum xs
Aucune de ces annotation de type n'est nécessaire ceci dit.

La décurryfication n'existe pas.

curry et uncurry ;)

Je compléterais en disant que la curryfication est vraiment un élément de design. Sans tomber dans le "troll" sur l'orienté objet, il est tout à fait possible d'avoir de la curryfication dans un context "orienté objet". On peut tout faire sans, mais des fois cela simplifie un peu. Je vivrais très bien en Haskell sans cette fonctionnalité, mais c'est souvent pratique.

Après, le fmt.Println est bien plus avancé (affiche et met en forme tous les type de Go, prends des paramètres variadique, etc)

Tu peux utiliser PyF.fmt pour avoir quelque chose de similaire en Haskell, avec formatage et interpolation.

Si vraiment tu veux mettre le type sur chaque variable, tu peux:

add (x :: Int) (y :: Int) = x + y
(Cela demande l'extension ScopedTypeVariables)

Si tu y tient aussi, tu peux tout écrire avec des tuples:

add' (x :: Int, y :: Int) = x + y
C'est là que curry et uncurry interviennent:

Prelude> :t add
add :: Int -> Int -> Int
Prelude> :t add'
add' :: (Int, Int) -> Int
Prelude> :t curry add'
curry add' :: Int -> Int -> Int
Prelude> :t uncurry (curry add')
uncurry (curry add') :: (Int, Int) -> Int
Prelude> :t uncurry add
uncurry add :: (Int, Int) -> Int
Prelude> :t curry (uncurry add)
curry (uncurry add) :: Int -> Int -> Int
Trouve le style qui te convient ;)

Maintenant tu demandes :

Une flèche implique une relation de cause à effet, ou une sorte de hiérarchie ; or rien de tel entre x et y, non ?

En fait si. On va disuter un peu plus théorie pour s'amuser. Ce n'est ABSOLUMENT pas utile pour faire du Haskell. La https://fr.wikipedia.org/wiki/Correspondance_de_Curry-Howard établit une relation entre type / implémentation et théorème / preuve. Dit autrement, un type est un théorème et son implémentation une preuve.

Reprenons l'exemple de add :: Int -> Int -> Int. C'est un théorème qui dit "Pour tout Int, pour tout autre Int, alors je peux associer un Int". Et la preuve est une preuve par construction avec la fonction + qui associe un Int à tout couple de deux Int.

Dans le cas précis cela ne sert à rien. D'autant que ce n'est pas tout à fait vrai en Haskell car on peut faire des fonctions non totales (i.e. qui ne marchent pas pour toutes leurs valeurs). Mais cela devient très amusant de lire des signatures de cette manière.

Un autre exemple: Int -> String est une fonction qui "à tout Int, associe une String". La preuve c'est la fonction de conversion vers string.

Ici python ne "transtype" pas, Il trie deux chaines de caractère ensemble en suivant un ordre lexicographique. C'est une relation d'ordre qui marche pas trop mal sur les chaines de caractères. On pourrait utiliser une autre relation d'ordre.

Maintenant l'algorithme lexicographique se base sur l'ordre des caractères entre eux et ici on peut se poser la question de cet ordre, qui pourrait être différent.

Nous on fait pareil et c'est S3 qui fait le cache aussi.

On a pas forcement testé cachix: toute notre infrastructure d'usine de code (gerrit, jenkins, gitlab, git-lfs) est déjà sur amazon, donc déployer un serveur de plus (configuré avec nix(os)) pour faire le cache était naturel.

Je comprend ton point de vue et j'avoue que mon manque d’intérêt pour la trace est surement due à mon manque de compétence.

Je n'ai pas le temps d'être bon en tout, alors j'essaye de devenir bon en VR (plat). Quand j'estimerais que je suis bon, je regarderais les autres discipline.

Bon sauts en tout cas ;)

Wuza c'est mort ;)

Ici aussi c'est tout pour le vertical (enfin plutôt sortir de l'avion ensemble et faire n'importe quoi). Pas moyen de trouver des gens pour briefer correctement et faire des points.

Je suis jaloux de vos moyens aériens, j'en ai marre de devoir changer de pays pour faire du 20+.

Cela y ressemble.

Autant pas mal de tes exemples me parlent, autant le coup du setup.py, je me sent personnellement agressé ;) Je pensais être qualifié en python, et je crois n'en avoir jamais écrit un. Bon, je devrais y arriver si j'ai le droit à une documentation.

La notion d'expert c'est super complexe et plus on monte en compétence dans une technologie, plus on se rend compte qu'elle est suffisamment vaste pour que on ne maîtrise pas tout.

Pour moi un expert c'est quelqu'un qui peut donner une réponse juste ou admettre qu'il ne sait pas.

Mais avec un prix aux US du jump ticket 30% moins chère, tes 200K ils valent bien plus. À ne pas négliger dans le calcul du coût de la vie.

(Ceci est une private joke. Je suis presque certain à 99.9% que Wawet76 et moi pratiquons le même loisir qui coûte un bras en France, et un peu moins chère aux USA ;)

Oui.

En même temps, le fait que ma femme paye aussi pour l'appartement implique que nous avons pu emprunter sur 10 ans et non pas sur 25 ans, mais j'aurais très bien pu assumer l'emprunt seul sur 20 ans. Et puis seul, sans enfants, je n'aurais pas choisi un appartement de cette taille en centre ville.

Moi oui, en gros, avec 100K à Lyon pour un foyer on vie très bien. Et oui, on est riche, je n'irais pas le nier.

T'as quoi comme appartement avec 600K euros à HK? Dit autrement, quel est le coût de la vie la bas, pour comparer tes 200K euros à mes 50K euros à Lyon ;)

Ici, 50K c'est assez pour avoir 100 mètres carrés d'appartement, dans une résidence avec jardin, piscine, garage, en centre ville à 10s du métro, avec 2 enfants à charge et des loisirs très coûteux. Bon, je triche, j'ai une femme qui le même niveau de vie que moi.

Quand j'étais "expert C++", je gagnais moins. Depuis que je suis expert Haskell, qualité, "devops", preuve formelle, je gagne un poil plus. Et je passe mon temps à croiser des gens qui me disent "mais, tu gagnes rien en fait, moi je gagne 200K à HK", et je cherche quel est le but de ces gens, à part me rendre triste parce que je me rend compte que j'ai raté ma vie et que si j'avais accepté les offres de google / facebook / pixar / younameit je gagnerais beaucoup plus?

Pour le coup, nix a aussi du sens dans une distro mutable puisque le boulot de nix c'est de te faire un environnent reproductible quel que soit la distro dans laquelle tu es.