Je vous concède bien volontiers que:
- Vous pouvez qualifier ma lecture de naïve dans le sens où je suis un béotien en matière de théorie des catégories, de même ma compréhension de la correspondance de Curry-Howard est sans doute la plus superficielle que vous puissiez concevoir.
- Ce que j'appelle résumé n'est que mon compte-rendu d'un point de vue purement calculatoire, j'assume complètement la possibilité voire la certitude d'être totalement passé à côté de la véritable valeur ajoutée de votre travail. Ce faisant je n'ai pas l'impression de minimiser la qualité de cet exposé, seulement j'en omet volontaire la partie (même si pour vous c'est cette partie qui constitue le véritable fond) dont j'ai la conviction (à tort ou à raison) qu'elle n'apportera aucun bénéfice calculatoire.
- La lisibilité est forcément un critère déterminant de la qualité c'est pourquoi je ne m'interdis pas les remarques sur la syntaxe concrête même si je sais que la syntaxe abstraite n'est pas en cause
Dire que le programmeur Anubis compile lui-même le filtrage c'est une remarque de syntaxe concrête, il est trop tôt pour dire la part due à la jeunesse de l'implémentation et celle due à votre intransigeance sur le filtrage. Je profite de l'occasion pour faire encore quelque remarque de syntaxe concrête:
Vous aurez reconnu une implémentation du tri fusion.Code:
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54define (List($T),List($T)) split (List($T) l) = if l is { [ ] then ([ ],[ ]), [ha . ta] then if ta is { [ ] then ([ha],[ ]), [hb . tb] then with w = split(tb), if w is { (u,v) then ([ha . u],[hb . v]) } } }. define List($T) merge ( ($T,$T) -> Bool less, List($T) l1, List($T) l2 ) = if l1 is { [ ] then l2, [h1 . t1] then if l2 is { [ ] then l1, [h2 . t2] then if less(h1,h2) then [h1 . merge(less,t1,l2)] else [h2 . merge(less,l1,t2)] } }. define List($T) msort ( ($T,$T) -> Bool less, List($T) l ) = if l is { [ ] then [ ], [ha . ta] then if ta is { [ ] then [ha], [hb . tb] then with w = split(l), if w is { (u,v) then merge(less,msort(less,u),msort(less,v)) } } }.
Je trouve cette expresssion désagréable:
Celle-ci serait davantage dans mes habitudes:Code:
2
3with w = split(tb), if w is { (u,v) then ([ha . u],[hb . v]) }
Et de façon similaire, à ceci:Code:
2
3with (u,v) = split(tb), ([ha . u],[hb . v])
Je préfèrerais cela:Code:
2
3
4
5
6
7
8
9
10
11
12if l1 is { [ ] then l2, [h1 . t1] then if l2 is { [ ] then l1, [h2 . t2] then ... } }
Voilà, j'en ai fini avec la syntaxe concrête.Code:
2
3
4
5
6
7
8
9if (l1,l2) is { ([ ],[ ]) then [], // pour disjoindre les deux gardes suivantes ([ ],_) then l2, (_,[ ]) then l1, ([h1 . t1],[h2 . t2]) then ... }
Au tour de la sémantique maintenant.
Sachant la rigueur qui vous caractérise, x n'est donc pas utilisable dans a.Citation:
with x = a, t
Notez que with x = a, t est un terme, et que son type est le type de t. Le terme t est la portée de la définition locale. Autrement-dit, le symbole x défini après le mot clef with n’est utilisable que dans le terme t.
C'est gênant, cela signifie que vous n'accordez pas aux données la contrepartie de la récursion que vous accordez aux fonctions. Cela a forcément un coût en terme d'expressivité, tôt ou tard une fonction récursive ne pourra pas être écrite parce qu'elle n'aura pas droit à sa donnée duale. En clair un traitement récursif ne sera pas spécifiable parce que sa sémantique sera rejetée. Ou, dit plus brutalement, Anubis n'est pas vraiment un langage récursif.
À mon grand regret ce code ne compile pas.Code:
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42read tools/basis.anubis type Expression: variable (Int32 bruijn), lambda (Expression body), apply (Expression f, Expression arg), let_in (Expression e, Expression body), letrec_in (Expression e, Expression body). type Value: error_bruijn_index, ok_function(Value -> Value). define Value eval ( Expression expr, List(Value) env ) = if expr is { variable(n) then if nth(n,env) is { failure then error_bruijn_index, success(v) then v } lambda(body) then ok_function((Value x) |-> eval(body, [x . env])) apply(f,arg) then if eval(f,env) is { error_bruijn_index then error_bruijn_index ok_function(f) then f(eval(arg,env)) } let_in(e,body) then eval(body, [eval(e,env) . env]) letrec_in(e,body) then with f = ok_function((Value x) |-> eval(e,[x . [f . env]])), eval(body, [f . env]) }.
La faute en incombe au f à droite du with:
Pourtant ce code me paraît légitime, le let rec a bien pour but d'étendre l'environnement env avec une nouvelle fonction qui pourra s'évaluer dans l'environnement étendu, si la récursion sur la donnée est impossible alors le let rec n'a pas de sémantique possible.Code:
2
3
4
Bien sûr il faut rejeter les cas pathologiques tels que:
Mais il faut tout de même autoriser les cas légitimes.Code:with x = x, x
Vous auriez anticipé cela si vous aviez programmé le compilateur Anubis en OCaml, au lieu de choisir un langage qui se rapproche au plus d'Anubis vous avez mis les mains dans le cambouis du C et il vous a caché vos vrais besoins. Je suis certain qu'en y réfléchissant vous trouverez dans les topos une raison pour laquelle le with devrait autoriser certaines formes de récursion. Et cette raison serait apparue bien plus vite à vos yeux si vous utilisiez OCaml. Sans doutes l'approche qui voit les besoins dans la beauté est la plus louable, mais l'approche duale qui voit la beauté dans les besoins est tout autant complémentaire car elle dissipe la fascination qui vous masque une beauté encore plus désirable.
