Discussion :

[SpiceGuid]

Les flèches sont nettement plus compliquées que les monades. En particulier, les équations sur les flèches (comme les "lois" des monades), c'est à dire les conditions de naturalité qu'une flèche doit nécessairement vérifier pour qu'elle se "comporte bien", sont complexes, et encore en mouvement (il est sorti un paper il y a un an ou deux apportant de nouvelles perspectives sur la question; pour ce qui est théorique, même en info c'est pas mal bleeding edge).

Si tu trouves les flèches plus naturelles que les monades, voici une image qui est peut-être pas complètement fausse, et qui pourrait t'aider : l'idée des flèches c'est d'avoir des machins de style 'a -> 'b, mais d'ajouter des fonctionnalités (du bling bling) en sous-main pour faire des choses magiques sans que le programmeur s'embête. Une flèche, ça peut rajouter du bling des deux côtés d'une fonction : en entrée ('a), et en sortie ('b); les fonctions permettent de "rajouter le bling de base" autour d'une fonction pure, de combiner des fonctions avec bling, etc.

Une monade, c'est un peu pareil, mais il n'y a du bling que d'un seul côté. Ce qui correspond à une ('a, 'b) arrow, c'est une 'a -> ('b monad). C'est une présentation (formellement, les flèches de Kleisli) qui n'est pas exactement celle des monades en Haskell, mais qui lui est équivalente. Dans ce point de vue, tu peux analyser bind et return ainsi :
- return : ajoute du bling "à la fin" (par analogie avec 'a -> 'b m)
- bind : permet de composer le bling (si tu as ('a -> 'b m) et ('b -> 'c m), pour obtenir un ('a -> 'c m) tu utilises un bind intermédiaire).

Selon cette vision des choses, les monades c'est des fonctions avec bling "seulement à la fin", alors que les arrows ont du bling des deux côtés. Ça explique pourquoi les monades sont plus simples; ça explique aussi pourquoi on a besoin des arrows : dans certain cas, on a besoin de bling aussi au début (par exemple pour des parsers, cf. le paper d'introductions aux arrows).

À vrai dire j'ai du mal à te suivre, tu sais sans doute mieux que moi ce dont tu parles, on peut sans doute faire ce que tu dis, mais ce n'est pas la motivation que j'y avais vue au départ.

Ton bling bling m'a l'air d'une nature passablement impérative.
J'ai l'impression que tu voudrais te servir des 'arrows' pour ne pas avoir à te salir les mains avec des effects de bord.

Je ne suis pas aussi puriste que ça, quand j'écris:

let v1 = e1 and v2 = e2 in e3

je peux compter sur le fait que e1 sera évalué avant e2,
je n'ai pas besoin de monades ou de arrows pour maquiller la nature séquencielle de la chose.

Les 'arrows' me sont venues d'une façon qui me paraît tout de même moins "torturée" que ta présentation le suggère.

Voilà un exemple, où je pense être proche des 'arrows' et les utiliser intuitivement (et en particulier sans m'attacher à vérifier les fameuses lois) sans que rien ne soit motivé par un quelconque bling bling.



B et D étants les milieux respectifs de AC et CE, je cherche à démontrer Thalès, c'est-à-dire l'égalité vectorielle AE = 2×BD.

Voilà ce que ça donne, d'abord je déclare un type vecteur muni d'une addition :

Code Caml :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
type 'a vect_expr =
  | Vect of 'a * 'a
  | Add  of 'a vect_expr * 'a vect_expr

Puis j'ajoute quelques équivalences et manipulations élémentaires:

Code Caml :

Sélectionner tout - Visualiser dans une fenêtre à part

1
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
(* AC = AB + BC *)
let split b = function
  | Vect(a,c) -> Add (Vect(a,b),Vect(b,c))
  | _ -> failwith "split"

(* AB + BC = AC *)
let merge = function
  | Add(Vect(a,b),Vect(c,d)) when b = c -> Vect(a,d)
  | _ -> failwith "merge"

(* u + v = v + u *)
let swap = function
  | Add(v1,v2) -> Add(v2,v1)
  | _ -> failwith "swap"

(* u + (v + w) =  (u + v) + w *)
let rotate_right = function
  | Add(v1,Add(v2,v3)) -> Add(Add(v1,v2),v3)
  | _ -> failwith "rotate_right"

(* (u + v) + w = u + (v + w) *)
let rotate_left = function
  | Add(Add(v1,v2),v3) -> Add(v1,Add(v2,v3))
  | _ -> failwith "rotate_left"

(* target u in u + v *)
let left f = function
  | Add(v1,v2) -> Add(f v1,v2)
  | _ -> failwith "left"

(* target v in u + v *)
let right f = function
  | Add(v1,v2) -> Add(v1,f v2)
  | _ -> failwith "right"

Les points qui m'intéressent:

Code Caml :

Sélectionner tout - Visualiser dans une fenêtre à part

type point =  A | B | C | D | E

Leurs propriétés :

• B est le milieu de A et C.
• D est le milieu de C et E.

D'où mes égalités vectorielles, dans un sens et puis dans l'autre :

Code Caml :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
let eq1 = [Vect(A,B),Vect(B,C);Vect(C,D),Vect(D,E)]
let eq2 = [Vect(B,C),Vect(A,B);Vect(D,E),Vect(C,D)]

Une substitution me permet de jongler avec ces quantités égales:

Code Caml :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
(* substitute equal values *)
let substitute eq v =
  List.assoc v eq

Un 'pipe' (pour diminuer le nombre de parenthèses) :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

let (<|) x f = f x

Ma preuve:

Code Caml :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
8
9
let thales_lemma v =
  v
  <| split B
  <| left (substitute eq1)
  <| right (split D)
  <| right (right (substitute eq2))
  <| right swap
  <| rotate_right
  <| left merge

D'accord, ça n'est pas très lisible, mais vous pouvez facilement vous convaincre que c'est bien la preuve recherchée :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
# Vect(A,E) <| thales_lemma;;
- : point vect_expr = Add (Vect (B, D), Vect (B, D))

Autrement dit on a bien l'égalité AE = 2×BD.

Il y a quelques redondances dans ma preuve.
On peut les éliminer à l'aide de l'opérateur de composition:

Code Caml :

Sélectionner tout - Visualiser dans une fenêtre à part

let (<<) f g v = g (f v)

La preuve "simplifiée" devient:

Code Caml :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
let thales_lemma v =
  v
  <| split B
  <| left (substitute eq1)
  <| right (split D << right (substitute eq2) << swap)
  <| rotate_right
  <| left merge

À tort ou à raison, j'ai cru reconnaître ces fameuse 'arrows', par contre je ne vois pas ici où est le bling bling dont tu parles.

Bref, je reste sur ce même sentiment selon lequel les monades seraient plutôt "impératives" tandis que les flêches seraient bien davantage "fonctionnelles".

[Jedai]

Je ne suis pas aussi puriste que ça, quand j'écris:

let v1 = e1 and v2 = e2 in e3

je peux compter sur le fait que e1 sera évalué avant e2,
je n'ai pas besoin de monades ou de arrows pour maquiller la nature séquencielle de la chose.

Uniquement si tu es dans un langage stricte ou s'il y a une dépendance de donnée directe.

Les 'arrows' me sont venues d'une façon qui me paraît tout de même moins "torturée" que ta présentation le suggère.

Voilà un exemple, où je pense être proche des 'arrows' et les utiliser intuitivement (et en particulier sans m'attacher à vérifier les fameuses lois) sans que rien ne soit motivé par un quelconque bling bling.

Les seules "Arrows" dans ton code sont les fonctions (->), littéralement ((->) respecte les lois des Arrows, mais il n'est pas le seul, il est l'exemple trivial (sans bling bling ajouté, pourrait-on dire)).

Bref, je reste sur ce même sentiment selon lequel les monades seraient plutôt "impératives" tandis que les flêches seraient bien davantage "fonctionnelles".

Peut-être que si tu savais de quoi tu parles plus formellement, ton sentiment serait différent ? En quoi exactement les monades comme [] ou Maybe sont-elles impératives ? Ou Reader ? Ou...

--
Jedaï

[SpiceGuid]

Les monades ne sont pas spécifiquement impératives, seulement on en a moins (plus du tout?) besoin dans un langage impératif/multiparadigmes.

Evidemment qu'on peut faire des monades 'pures' et des 'arrows' pleines de bling bling impératif cependant, sorties du contexte Haskell, les 'arrows' me paraissent plus nobles dans leur motivation initiale.

Les seules "Arrows" dans ton code sont les fonctions (->), littéralement

Je suis bien conscient de ne pas avoir implémenté cette interface:

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
module type Arrow = sig
  type ('a,'b) arrow
  val  make : ('a -> 'b) -> ('a,'b) arrow 
  val  (>>>) : ('a,'b) arrow -> ('b,'c) arrow -> ('a,'c) arrow
  val  first : ('a,'b) arrow -> ('a * 'c,'b * 'c) arrow 
end

Cependant ça ne suffit pas à me convaincre que mon code n'a rien à voir avec les 'arrows', peut être que j'ai simplement utilisé quelque chose de similaire sans chercher à le réifier (tout réifier c'est une manie de la POO). Mais comme, effectivement, je ne sais pas de quoi je parle, je n'en suis pas convaincu non plus.

[SpiceGuid]

Bon, je suis toujours d'avis que le triangle ACE est une catégorie où:

• l'identité est le vecteur nul
• je peux construire une flèche (dans cette catégorie) à partir de deux points
• la composition est la relation de Chasles, elle est associative

Là où j'hésite encore c'est sur la fonction split (décomposition par la relation de Chasles) dont l'implémentation est :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

Vect(a,b) -> Add (Vect(a,c),Vect(c,b))

À comparer avec la signature de first :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

('a,'b) arrow -> ('a * 'c,'b * 'c) arrow

On voit bien que si j'ajoutais Neg v pour construire l'opposé d'un vecteur v alors split pourrait s'implémenter comme ceci :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

Vect(a,b) -> Add (Vect(a,c),Neg(Vect(b,c)))

Superficiellement, il y a une certaine ressemblance, là où ça diffère c'est qu'un point est un objet, pas un type.
Il y a de quoi avoir une présomption ou bien je fais trop marcher mon imagination ?

[gasche]

Tu te trouves effectivement dans une catégorie, mais tu ne peux pas pour autant utiliser l'interface des Arrows, ne serait-ce que parce que ta catégorie n'a pas de produit.

Par ailleurs, les Arrows permettent en Haskell de représenter des flèches "au niveau des types", c'est à dire qui sont des extensions 'naturelles' des flèches dans la catégorie dont les objets sont des types, qui sont des fonctions d'un type vers un autre (avec des points techniques discutables liés entre autres à la paresse qui (pour une fois ?) fait chier les théoriciens, et que je ne maîtrise pas du tout) : en particulier elles demandent une manière d'intégrer une fonction "pure" ('a -> 'b) dans tes flèches, ce qui est évidemment impossible dans ton cas.

En gros : oui c'est une catégorie, donc oui ça ressemble, mais non tu ne pourras pas utiliser le concept de Arrows (ou de monades) dans ton cas, parce qu'il s'utilise en Haskell seulement dans des cas appliqués et particuliers dont tu ne fais pas partie. S'il existait un concept en Haskell permettant de "représenter une catégorie en général", il n'aurait sans doute pas grande utilité puisque, comme un peu n'importe quoi peut se représenter avec des catégories, il ne pourrait s'appuyer sur aucune propriété particulière.

[SpiceGuid]

Alors, en gros, je suis en présence de flèches, mais au sens le plus naïf, et donc il n'y a rien de particulier que je puisse faire ici et que je ne puisse pas faire sur la base de n'importe quel graphe orienté qui aurait le bonheur d'être une catégorie (ce qui, au vu du peu de conditions requises, n'est pas un exploit).

Merci à tous mes amis (qui m'ont soutenu dans mon vaillant effort vers la nullitude relative).
(mon premier depuis un moment)