"Le problème de l'égalité structurelle en OCaml c'est qu'elle peut être indécidable, et partir dans un calcul sans fin :"
On dirait que la principale raison du coté indécidable est la récursion. C'est pour cela que je parle de graphe acyclique. Il suffit de traiter les références différemment des définitions, cela permet de transformer la plus part des codes/données en graphes acycliques.
Selon le système de types (sa « puissance » expressive) l'existence d'une preuve d'une assertion peut devenir indécidable
Oui, d'où la recherche d'un sous-ensemble dans lequel il est possible de prouver quelques choses d'utile, et ne surtout pas regarder le cas général.
Le principe même de mon langage était de pousser le principe du typage le plus loin possible, car si il est impossible de "prouver" un code dans le cas général, tu peux prouver beaucoup de choses structurellement. Donc, l'idée était de voir jusqu'où on pouvait aller dans le typage statique.
On peut rajouter que je détestais le principe même du metamodèle UML qui empêche de faire des trucs aussi simple que de fixer la valeur d'une propriété dans un raffinement. Donc, j'ai mis les littéraux au même niveau que leur type.
La syntaxe n'est pas fixé, l'idée était plutôt un truc manipulable par des commandes externes (editeur texte ou graphique) ou un format de fichier type XML mais qui permet de définir des graphs acyclique avec le même langage pour le schéma.
type t =
(*Literals*)
| LInt of int
| LString of string
| LFloat of float
(*Internal type*)
| Integer
| Float
| String
(*Op*)
| And of t * t
| Or of t * t
| Xor of t list
(* Nommé *)
| Name of string
(* Pointeur avec un path *)
| Ref of string list (* TODO: adding integer index ref *)
(* Multiplicité *)
| Mult of int * int
J'avais tenté le gadt, mais j'avais vraiment du mal :
type _ term =
(*Literals*)
| LInt : int -> int term
| LString : string -> string term
| LFloat : float -> float term
(*Internal type*)
| Integer : int term
| Float : float term
| String : string term
(*Op*)
| And : 'a term * 'a term -> 'a term
| Or : _ term * _ term -> _ term
| Xor : 'a term list-> _ term (*agregation also used for array*)
(*Nommé *)
| Name : string -> _ term
(*Pointeur avec un path*)
| Ref : string list -> _ term
(*Multiplicité*)
| Mult : int * int -> 'a term J'avais aussi envie d'ajouter un "Not" pour faire l'inverse de "And", cela permet de faire une logique plus complète (j'y ai pensé après avoir lu logicomix). Mais le "And" n'est pas un "and" (je l'ai appelé comme ça par rapport à "|" du type sum), c'est plus un "Sont du même type" genre un "~", c'est un blanc dans ma mini syntaxe. Le "Xor" c'est le "*" de ocaml (définit par le retour à la ligne et la tabulation). Le moyen de faire les tuples et les array.
Est-ce que tu connais un moyen d'exprimer un "ou" avec un gadt?
Du style :
| Or : 'a term * 'b term -> ('a| 'b) term
Et est-ce qu'il existe un moyen de faire une égalité structurelle, par exemple pour considérer de même type, une structure ou une liste qui contient le même nombre d'argument de type compatible entre eux ?
Je comprend beaucoup mieux. L'idée est que le fold retourne une liste complexe d'éléments qui sont analysé ensuite. Au lieu de tout faire en même temps, ce qui est très pénible, si le fold retourne juste vrai ou faux.
Le principe de conception est sympa. Mais c'est toujours plus simple de partir d'un exemple. Comme Dell, vous pourriez montrer des configs à modifier au lieu de présenter un truc vide.
J'ai pu mettre 2 cpus différents sur la même machine, cela me semble louche quand même.
Je n'ai pas vu d'aide pour choisir (caractéristiques des cpu par exemple). Je n'ai pas vu de validation de configuration par exemple, pour montrer si il manque un truc. L'idéal serait un code couleur sur le dessin en cas de manque, et un symbole entre le dessin et la sélection possible (d'ailleurs, je n'ai pas trouvé ce que l'on peut mettre dans la grande case en bas à droite sur un serveur).
Sinon, c'est assez souple, et l'idée de conserver les configurations déjà faites est bonne.
On ne peut pas créer 2 rack ? Si je créais un serveur dans le 2ième rack, je retourne dans la définition du 1er.
On est en France et par définition on achète pas une innovation qu'on a pas créée soit même (ou qui ne vient pas de très loin),
Dans le logiciel, c'est pareil. Une innovation française est plus facile à vendre en Chine et en Amérique, qu'en France. Il faut avoir fait ses preuves ailleurs d'abord.
J'ai vu la vidéo. En plus des truc EMF, pour moi-même, j'ai codé un mini langage EDSL en ocaml pour éviter de devoir réinventer la roue. Mais le typage est différente de celui de ocaml, cela ne peut pas s'exprimer avec un gadt. Je l'ai donc recodé à la main.
D'ailleurs, est-ce que dans les gadt, on peut mettre no propre type fantome ?
J'ai toujours vu des trucs comme ça :
type _ term =
| Lit : int -> int term
| Bool : bool -> bool term
| Add : int term * int term -> int term
| Neg : int term -> int term
| If : bool term * 'a term * 'a term -> 'a term
int/bool et jamais des type définit, qui n'ont d'utilité que pour ajouter un "tag" sur le résultat. (imagine un type "neverzero int" uniquement accepté par la division). L'idéal serait de pouvoir jouer avec des ensembles de variant, mais je ne crois pas que c'est possible.
Je ne comprend toujours pas. Je dois être un peu lent, ou alors je n'ai pas eu affaire aux mêmes cas d'utilisation.
Je me dis la même chose en lisant les pattern de code plus haut :)
Comment tu fais en parcourant l'arbre ? Mon algorithme débile trouve une chaine de contraintes … et après il faut résoudre, mais en tout cas il la trouve.
En fait, c'est ton algo débile que je n'ai pas compris. Est-ce que tu peux reprendre mon exemple, et montrer ce qui il y aurait dans les listes, et comment se fait la vérification ?
En pratique, pour ocaml, ils récupèrent les contraintes de types, et font un algorithme d'unification un peu amélioré pour résoudre le problème du polymorphisme et trouver les types minimaux des expressions. Mais ils récupèrent « d'un coup » toutes les contraintes (en éliminant peut-être celles qui sont triviales localement).
L'exemple ressemble à du C, mais tu peux le voir aussi simplement comme une description de donné.
Un DSL, sans référence, c'est vraiment un gros jouet inutile. En gros, cela veut dire que tu ne peux pas définir un truc dans ton langage, pour le réutiliser ensuite.
(pour info, je bosse dans le domaine, autour des objet EMF d'eclipse, et des stéréotypes de sysml)
Tu oublis le temps qu'il faut pour complètement remplacer linkedin, il y a un effet de latence. Le site est la référence absolue dans le monde, il n'y a pas de concurrent.
Si tu as un :
typedef int toto_t;
...
toto_t toto = 1; Tu va construire 2 listes, avec ([toto_t -> int, toto -> toto_t],[ toto -> 1]) et ensuite comment tu fais de façon performante le lien "1 <- toto <- toto_t <- int" pour vérifier que c'est bon ?
Essayes de prendre un arbre plus grand, l'idéal serait de faire une courbe en fonction de n, tu pourrais voir si les coubres sont parallèle ou si elles vont se croiser, ou encore, si il y a un cout d'init très élevé pour un cas particuliers.
Par type, je disais que tu as une définition dans un coin de ton arbre, qui a un nom "type_t".
Ailleurs, dans ton arbre, tu as un machin qui fait référence à "type_t". Pour vérifier que l'expression est juste, il faut aller chercher "type_t", ce qui empèche un simple parcourt d'arbre. Il faut le parcourt d'arbre, plus une fonction qui recherche le type dans l'arbre depuis la racine. C'est plus lent, et plus complexe, surtout si l'arbre est énorme.
Je pensais vraiment à un model, de l'ingénierie des modèles, c'est à dire une ensemble de classe qui respecte un diagramme de classe type UML. Donc, qui réutilise des définitions pour créer de nouveaux objets.
Pour ton explication, j'ai compris ton typage de fonction comme ayant simplement un nombre d'argument local sur une fonction, et non la réutilisation d'une définition qui est "ailleurs". La deuxième partie de l'explication, je suis vraiment passé à coté par contre…:/
Il faut que je relise plus doucement l'article. Mais les variants ont été critiqué, car ils ne permettent plus le principal avantage des types sommes : l’exhaustivité de leur usage.
Il suffit de rajouter un élément pour que tous les filtres soient en erreur à la compilation. Ce n'est plus toujours le cas avec des variants, le compilo n'arrive pas à évaluer tous les cas. Pour le refactoring, c'est très puissant.
C'était un gars de ocaml pro qui m'avait dit que beaucoup d'usagers de variants pour des AST avaient changé d'avis.
J'ai du mal à comprendre l’intérêt d'une fonction générique comme fold(). Le nombre d'argument est égal au nombre d'argument du type expr. Cela permet ici de pouvoir gérer plus facilement des "exécutions" différente.
Mais le problème concerne surtout l'ajout d'élément au type. Cela implique à chaque fois l'ajout d'un argument au fold, non ?
"Pour un système de type par exemple, on peut faire remonter le type de chaque expression, ainsi que toutes les contraintes de types qui sont dans les sous-expressions, et l'ensemble des variables libres. Ces informations devraient normalement être suffisantes pour pouvoir déterminer tous les types."
Oui, mais tu as besoin de l'ast, dans ce cas, pour aller chercher tous les types en question.
ok, je comprend mieux. Mais cela ne simplifie pas grand chose par rapport à un AST "classique" ("deep").
En fait, tu ne fais pas grand chose avec juste une composition structurelle. Un truc que tu as souvent besoin, c'est une référence vers un autre nœud de l'arbre et de pouvoir avoir accès à son contenu (typage, association, connecteur,…).
Si je reprend le code d'exemple :
ça c'est bien un gadt ?
type 'a exp_dic =
{lit : int -> 'a;
neg : 'a -> 'a;
add : 'a * 'a -> 'a};;
ça c'est la définition de la sémantique de "Lit" qui retourne une fonction de construction d'un type ?
let lit : int -> exp = fun x ->
{expi = fun d -> d.lit x}
Que signifie la syntaxe : {expi = …} ? C'est la création d'un type avec un champs expi ?
ça c'est l'éval :
let eval1 : exp -> int = fun {expi = e} ->
e {lit = (fun x -> x);
neg = (fun e -> - e);
add = (fun (e1,e2) -> e1 + e2)};;
Que signifie la syntaxe "fun {expi = e}" ? et qu'est-ce que le terme "e {…}" ?
J'ai toujours rien compris non plus. Mais je tente de comprendre pour simplifier une fonction de vérification du modèle et pas seulement d’exécution (ou alors une exécution qui rend vrai/faux). Le modèle récursif est élégant, mais devient vite imbitable avec des arbres.
De mémoire, pour le bitcoin, tu dois trouver un nombre 128 bits, qui, ajouté à un bloc donne un hash SHA-256 avec un nombre déterminé de bit à zéro.
Donc, tu testes un grand nombre de nombre pour en trouver un.
" Si toutes les transactions jamais faites par BC sont gardées sur une chaîne, quelle taille fait cette chaîne aujourd'hui?"
Qq centaine de Go de mémoire.
" Comment peut-on demander à un réseau de 1 milliards de noeuds de rester synchronisé sans que des bouts soient ajoutés ici et là dans plusieurs branches?"
Par un système de vote à la majorité, et une vérification des autres blocs et détection d'erreur qui ferait refuser les blocs douteux;
" Comment peut-on savoir si la majorité du réseau approuve la transaction sans savoir combien de noeuds existent?"
sur bitcoin, on attend juste la réponse de quelques noeuds pas de tous. Cette latence est en train de devenir un problème. (gros mineur en chine avec peu de bande passante)
" Si un État créé 10millions d'"utilisateurs" et donc autant de noeuds, peut-il saborder le système en invalidant les transactions qui lui déplaisent?"
Oui si il dispose plus de 50% de la puissance de calcul, mais cela ne serait pas discret. De plus, les noeuds sont des asic plus des PC ou même des cartes graphiques puissantes.
" On dit que les utilisateurs restent anonymes derrière une clé publique, mais si l'autre partie identifie l'utilisateur de la clé, il peut ensuite pister toutes ses transactions en surveillant la chaîne?"
Oui, c'est la différence entre le pseudonymat et l'anonymat.
"Et pour finir: comment on fait un système d'identification avec ça??"
Si tu connais le système de certificat TLS actuelle, tu sais qu'une clef est connu si elle est signé par une compagnie dont les clefs sont dans les navigateurs. Il faut donc leur faire confiance. Ici, la clef est simplement stocké dans la blockchain.
[^] # Re: Dans l'art voluptueuse de ne rien comprendre
Posté par Nicolas Boulay (site web personnel) . En réponse au journal EDSL et F-algèbres. Évalué à 2.
On dirait que la principale raison du coté indécidable est la récursion. C'est pour cela que je parle de graphe acyclique. Il suffit de traiter les références différemment des définitions, cela permet de transformer la plus part des codes/données en graphes acycliques.
Oui, d'où la recherche d'un sous-ensemble dans lequel il est possible de prouver quelques choses d'utile, et ne surtout pas regarder le cas général.
"La première sécurité est la liberté"
[^] # Re: Dans l'art voluptueuse de ne rien comprendre
Posté par Nicolas Boulay (site web personnel) . En réponse au journal EDSL et F-algèbres. Évalué à 2.
Le principe même de mon langage était de pousser le principe du typage le plus loin possible, car si il est impossible de "prouver" un code dans le cas général, tu peux prouver beaucoup de choses structurellement. Donc, l'idée était de voir jusqu'où on pouvait aller dans le typage statique.
On peut rajouter que je détestais le principe même du metamodèle UML qui empêche de faire des trucs aussi simple que de fixer la valeur d'une propriété dans un raffinement. Donc, j'ai mis les littéraux au même niveau que leur type.
L'idée est de pouvoir écrire un truc comme :
La syntaxe n'est pas fixé, l'idée était plutôt un truc manipulable par des commandes externes (editeur texte ou graphique) ou un format de fichier type XML mais qui permet de définir des graphs acyclique avec le même langage pour le schéma.
https://github.com/nicolasboulay/cherry-lang/blob/master/src/grape.ml
J'avais tenté le gadt, mais j'avais vraiment du mal :
type _ term =
(*Literals*)
| LInt : int -> int term
| LString : string -> string term
| LFloat : float -> float term
(*Internal type*)
| Integer : int term
| Float : float term
| String : string term
(*Op*)
| And : 'a term * 'a term -> 'a term
| Or : _ term * _ term -> _ term
| Xor : 'a term list-> _ term (*agregation also used for array*)
(*Nommé *)
| Name : string -> _ term
(*Pointeur avec un path*)
| Ref : string list -> _ term
(*Multiplicité*)
| Mult : int * int -> 'a term
"La première sécurité est la liberté"
[^] # Re: Dans l'art voluptueuse de ne rien comprendre
Posté par Nicolas Boulay (site web personnel) . En réponse au journal EDSL et F-algèbres. Évalué à 2.
Est-ce que tu connais un moyen d'exprimer un "ou" avec un gadt?
Du style :
| Or : 'a term * 'b term -> ('a| 'b) term
Et est-ce qu'il existe un moyen de faire une égalité structurelle, par exemple pour considérer de même type, une structure ou une liste qui contient le même nombre d'argument de type compatible entre eux ?
"La première sécurité est la liberté"
[^] # Re: Dans l'art voluptueuse de ne rien comprendre
Posté par Nicolas Boulay (site web personnel) . En réponse au journal EDSL et F-algèbres. Évalué à 2.
ok, je n'avais pas du utiliser la bonne syntaxe quand j'avais essayé. Va falloir que je reprennes mon code :)
"La première sécurité est la liberté"
[^] # Re: Pareil partout
Posté par Nicolas Boulay (site web personnel) . En réponse au journal Quel modèle économique pour l'Open Hardware ?. Évalué à 3.
Que des trucs venu par d'énorme structures étatiques. Or ce n'est plus du tout la façon d'innover d'aujourd'hui, c'est bien trop lent.
"La première sécurité est la liberté"
[^] # Re: Pareil partout
Posté par Nicolas Boulay (site web personnel) . En réponse au journal Quel modèle économique pour l'Open Hardware ?. Évalué à 4.
Dans ce cas là, tu n'as pas d'innovations à vendre.
L'innovation vient rarement d'énarque ou de science-po, mais de scientifiques.
"La première sécurité est la liberté"
[^] # Re: Dans l'art voluptueuse de ne rien comprendre
Posté par Nicolas Boulay (site web personnel) . En réponse au journal EDSL et F-algèbres. Évalué à 2.
Je comprend beaucoup mieux. L'idée est que le fold retourne une liste complexe d'éléments qui sont analysé ensuite. Au lieu de tout faire en même temps, ce qui est très pénible, si le fold retourne juste vrai ou faux.
Merci.
"La première sécurité est la liberté"
[^] # Re: test du site
Posté par Nicolas Boulay (site web personnel) . En réponse au journal Quel modèle économique pour l'Open Hardware ?. Évalué à 2.
-> fait il perd le fait que j'avais choisie un rugged, et non un rack V1.
"La première sécurité est la liberté"
# test du site
Posté par Nicolas Boulay (site web personnel) . En réponse au journal Quel modèle économique pour l'Open Hardware ?. Évalué à 2. Dernière modification le 16 juin 2016 à 15:35.
Le principe de conception est sympa. Mais c'est toujours plus simple de partir d'un exemple. Comme Dell, vous pourriez montrer des configs à modifier au lieu de présenter un truc vide.
J'ai pu mettre 2 cpus différents sur la même machine, cela me semble louche quand même.
Je n'ai pas vu d'aide pour choisir (caractéristiques des cpu par exemple). Je n'ai pas vu de validation de configuration par exemple, pour montrer si il manque un truc. L'idéal serait un code couleur sur le dessin en cas de manque, et un symbole entre le dessin et la sélection possible (d'ailleurs, je n'ai pas trouvé ce que l'on peut mettre dans la grande case en bas à droite sur un serveur).
Sinon, c'est assez souple, et l'idée de conserver les configurations déjà faites est bonne.
On ne peut pas créer 2 rack ? Si je créais un serveur dans le 2ième rack, je retourne dans la définition du 1er.
"La première sécurité est la liberté"
# Pareil partout
Posté par Nicolas Boulay (site web personnel) . En réponse au journal Quel modèle économique pour l'Open Hardware ?. Évalué à 3.
Dans le logiciel, c'est pareil. Une innovation française est plus facile à vendre en Chine et en Amérique, qu'en France. Il faut avoir fait ses preuves ailleurs d'abord.
"La première sécurité est la liberté"
[^] # Re: Dans l'art voluptueuse de ne rien comprendre
Posté par Nicolas Boulay (site web personnel) . En réponse au journal EDSL et F-algèbres. Évalué à 2.
J'ai vu la vidéo. En plus des truc EMF, pour moi-même, j'ai codé un mini langage EDSL en ocaml pour éviter de devoir réinventer la roue. Mais le typage est différente de celui de ocaml, cela ne peut pas s'exprimer avec un gadt. Je l'ai donc recodé à la main.
D'ailleurs, est-ce que dans les gadt, on peut mettre no propre type fantome ?
J'ai toujours vu des trucs comme ça :
type _ term =
| Lit : int -> int term
| Bool : bool -> bool term
| Add : int term * int term -> int term
| Neg : int term -> int term
| If : bool term * 'a term * 'a term -> 'a term
int/bool et jamais des type définit, qui n'ont d'utilité que pour ajouter un "tag" sur le résultat. (imagine un type "neverzero int" uniquement accepté par la division). L'idéal serait de pouvoir jouer avec des ensembles de variant, mais je ne crois pas que c'est possible.
"La première sécurité est la liberté"
[^] # Re: Dans l'art voluptueuse de ne rien comprendre
Posté par Nicolas Boulay (site web personnel) . En réponse au journal EDSL et F-algèbres. Évalué à 2.
Je me dis la même chose en lisant les pattern de code plus haut :)
En fait, c'est ton algo débile que je n'ai pas compris. Est-ce que tu peux reprendre mon exemple, et montrer ce qui il y aurait dans les listes, et comment se fait la vérification ?
Euh…
"La première sécurité est la liberté"
[^] # Re: Dans l'art voluptueuse de ne rien comprendre
Posté par Nicolas Boulay (site web personnel) . En réponse au journal EDSL et F-algèbres. Évalué à 2.
L'exemple ressemble à du C, mais tu peux le voir aussi simplement comme une description de donné.
Un DSL, sans référence, c'est vraiment un gros jouet inutile. En gros, cela veut dire que tu ne peux pas définir un truc dans ton langage, pour le réutiliser ensuite.
(pour info, je bosse dans le domaine, autour des objet EMF d'eclipse, et des stéréotypes de sysml)
à propos des type fantômes j'ai retrouvé ça : https://linuxfr.org/users/montaigne/journaux/les-types-fantomes.
Si tu réutilises ton système de typage de ton langage hote, tu ne peux pas faire "autre chose", ce qui est très limitant.
"La première sécurité est la liberté"
[^] # Re: Une question de choix
Posté par Nicolas Boulay (site web personnel) . En réponse au journal Rachat de LinkedIn par Microsoft pour 26 milliards de dollars. Évalué à 3.
Tu oublis le temps qu'il faut pour complètement remplacer linkedin, il y a un effet de latence. Le site est la référence absolue dans le monde, il n'y a pas de concurrent.
"La première sécurité est la liberté"
[^] # Re: Dans l'art voluptueuse de ne rien comprendre
Posté par Nicolas Boulay (site web personnel) . En réponse au journal EDSL et F-algèbres. Évalué à 2.
Si tu as un :
typedef int toto_t;
...
toto_t toto = 1;
"La première sécurité est la liberté"
[^] # Re: C'est bien la peine !
Posté par Nicolas Boulay (site web personnel) . En réponse au journal EDSL et F-algèbres. Évalué à 2.
Essayes de prendre un arbre plus grand, l'idéal serait de faire une courbe en fonction de n, tu pourrais voir si les coubres sont parallèle ou si elles vont se croiser, ou encore, si il y a un cout d'init très élevé pour un cas particuliers.
"La première sécurité est la liberté"
[^] # Re: Dans l'art voluptueuse de ne rien comprendre
Posté par Nicolas Boulay (site web personnel) . En réponse au journal EDSL et F-algèbres. Évalué à 3.
Par type, je disais que tu as une définition dans un coin de ton arbre, qui a un nom "type_t".
Ailleurs, dans ton arbre, tu as un machin qui fait référence à "type_t". Pour vérifier que l'expression est juste, il faut aller chercher "type_t", ce qui empèche un simple parcourt d'arbre. Il faut le parcourt d'arbre, plus une fonction qui recherche le type dans l'arbre depuis la racine. C'est plus lent, et plus complexe, surtout si l'arbre est énorme.
Je pensais vraiment à un model, de l'ingénierie des modèles, c'est à dire une ensemble de classe qui respecte un diagramme de classe type UML. Donc, qui réutilise des définitions pour créer de nouveaux objets.
Pour ton explication, j'ai compris ton typage de fonction comme ayant simplement un nombre d'argument local sur une fonction, et non la réutilisation d'une définition qui est "ailleurs". La deuxième partie de l'explication, je suis vraiment passé à coté par contre…:/
"La première sécurité est la liberté"
[^] # Re: C'est bien la peine !
Posté par Nicolas Boulay (site web personnel) . En réponse au journal EDSL et F-algèbres. Évalué à 3.
Il faut que je relise plus doucement l'article. Mais les variants ont été critiqué, car ils ne permettent plus le principal avantage des types sommes : l’exhaustivité de leur usage.
Il suffit de rajouter un élément pour que tous les filtres soient en erreur à la compilation. Ce n'est plus toujours le cas avec des variants, le compilo n'arrive pas à évaluer tous les cas. Pour le refactoring, c'est très puissant.
C'était un gars de ocaml pro qui m'avait dit que beaucoup d'usagers de variants pour des AST avaient changé d'avis.
"La première sécurité est la liberté"
[^] # Re: Une question de choix
Posté par Nicolas Boulay (site web personnel) . En réponse au journal Rachat de LinkedIn par Microsoft pour 26 milliards de dollars. Évalué à 7.
Tu peux aussi faire en sorte que les meilleurs CV ne reçoivent plus d'offres concurrentes….
"La première sécurité est la liberté"
[^] # Re: C'est bien la peine !
Posté par Nicolas Boulay (site web personnel) . En réponse au journal EDSL et F-algèbres. Évalué à 3.
J'ai du mal à comprendre l’intérêt d'une fonction générique comme fold(). Le nombre d'argument est égal au nombre d'argument du type expr. Cela permet ici de pouvoir gérer plus facilement des "exécutions" différente.
Mais le problème concerne surtout l'ajout d'élément au type. Cela implique à chaque fois l'ajout d'un argument au fold, non ?
"La première sécurité est la liberté"
[^] # Re: Dans l'art voluptueuse de ne rien comprendre
Posté par Nicolas Boulay (site web personnel) . En réponse au journal EDSL et F-algèbres. Évalué à 3.
Oui, mais tu as besoin de l'ast, dans ce cas, pour aller chercher tous les types en question.
"La première sécurité est la liberté"
[^] # Re: Dans l'art voluptueuse de ne rien comprendre
Posté par Nicolas Boulay (site web personnel) . En réponse au journal EDSL et F-algèbres. Évalué à 2.
ok, je comprend mieux. Mais cela ne simplifie pas grand chose par rapport à un AST "classique" ("deep").
En fait, tu ne fais pas grand chose avec juste une composition structurelle. Un truc que tu as souvent besoin, c'est une référence vers un autre nœud de l'arbre et de pouvoir avoir accès à son contenu (typage, association, connecteur,…).
"La première sécurité est la liberté"
[^] # Re: Dans l'art voluptueuse de ne rien comprendre
Posté par Nicolas Boulay (site web personnel) . En réponse au journal EDSL et F-algèbres. Évalué à 2.
Si je reprend le code d'exemple :
ça c'est bien un gadt ?
type 'a exp_dic =
{lit : int -> 'a;
neg : 'a -> 'a;
add : 'a * 'a -> 'a};;
ça c'est la définition de la sémantique de "Lit" qui retourne une fonction de construction d'un type ?
let lit : int -> exp = fun x ->
{expi = fun d -> d.lit x}
Que signifie la syntaxe : {expi = …} ? C'est la création d'un type avec un champs expi ?
ça c'est l'éval :
let eval1 : exp -> int = fun {expi = e} ->
e {lit = (fun x -> x);
neg = (fun e -> - e);
add = (fun (e1,e2) -> e1 + e2)};;
Que signifie la syntaxe "fun {expi = e}" ? et qu'est-ce que le terme "e {…}" ?
"La première sécurité est la liberté"
[^] # Re: Dans l'art voluptueuse de ne rien comprendre
Posté par Nicolas Boulay (site web personnel) . En réponse au journal EDSL et F-algèbres. Évalué à 7.
J'ai toujours rien compris non plus. Mais je tente de comprendre pour simplifier une fonction de vérification du modèle et pas seulement d’exécution (ou alors une exécution qui rend vrai/faux). Le modèle récursif est élégant, mais devient vite imbitable avec des arbres.
"La première sécurité est la liberté"
[^] # Re: J'ai jamais tout compris aux chaines de blocs!
Posté par Nicolas Boulay (site web personnel) . En réponse au journal Microsoft s'intéresse au blockchain. Évalué à 10.
" Quand on mine, on résout quoi exactement?"
De mémoire, pour le bitcoin, tu dois trouver un nombre 128 bits, qui, ajouté à un bloc donne un hash SHA-256 avec un nombre déterminé de bit à zéro.
Donc, tu testes un grand nombre de nombre pour en trouver un.
" Si toutes les transactions jamais faites par BC sont gardées sur une chaîne, quelle taille fait cette chaîne aujourd'hui?"
Qq centaine de Go de mémoire.
" Comment peut-on demander à un réseau de 1 milliards de noeuds de rester synchronisé sans que des bouts soient ajoutés ici et là dans plusieurs branches?"
Par un système de vote à la majorité, et une vérification des autres blocs et détection d'erreur qui ferait refuser les blocs douteux;
" Comment peut-on savoir si la majorité du réseau approuve la transaction sans savoir combien de noeuds existent?"
sur bitcoin, on attend juste la réponse de quelques noeuds pas de tous. Cette latence est en train de devenir un problème. (gros mineur en chine avec peu de bande passante)
" Si un État créé 10millions d'"utilisateurs" et donc autant de noeuds, peut-il saborder le système en invalidant les transactions qui lui déplaisent?"
Oui si il dispose plus de 50% de la puissance de calcul, mais cela ne serait pas discret. De plus, les noeuds sont des asic plus des PC ou même des cartes graphiques puissantes.
" On dit que les utilisateurs restent anonymes derrière une clé publique, mais si l'autre partie identifie l'utilisateur de la clé, il peut ensuite pister toutes ses transactions en surveillant la chaîne?"
Oui, c'est la différence entre le pseudonymat et l'anonymat.
"Et pour finir: comment on fait un système d'identification avec ça??"
Si tu connais le système de certificat TLS actuelle, tu sais qu'une clef est connu si elle est signé par une compagnie dont les clefs sont dans les navigateurs. Il faut donc leur faire confiance. Ici, la clef est simplement stocké dans la blockchain.
"La première sécurité est la liberté"