Discussion :

[Garulfo]

+1, surtout en version online, pour qu'on puisse le lire depuis n'importe où

Comme d'un endroit où il n'y a pas l'Internet ? :O

[gorgonite]

Comme d'un endroit où il n'y a pas l'Internet ? :O

je le savais, j'aurais du rester en Chine, toute le monde est méchant avec moi ici

[SpiceGuid]

Pour ceux que cela intéresse, j'ai mis en ligne une archive de Charity, avec les exécutables pour Linux et Windows, les exemples, et la documentation convertie en pdf.
Charity est un langage d'inspiration catégorique.

Charity Home Page:
http://pll.cpsc.ucalgary.ca/charity1/www/home.html

Premières impressions:

• c'est un langage 'expérimental', les opérations sur les booléens et les entiers unaires sont définies dans le fichier PRELUDE.ch
• toutes les fonctions sont totales, le prélude exporte un type Maybe
• l'application semble ne pas exister, il n'y a que des fonctions et la juxtaposition c'est la composition de fonction (g f = g ◦ f)
• autrement le style est le même qu'en Anubis, pour les types inductifs la conditionnelle est notée {...} et le catamorphisme est noté {|...|} (barbed wire)
• pour les types coinductifs le dual de la conditionnelle est noté (...) et l'anamorphisme est noté (|...|) (lenses)
• un caractère spécial permet de réaliser le paramorphisme ainsi que son dual l'apomorphisme
• le foncteur d'un type t associé à une fonction f est noté t{f}

Pour charger le fichier prélude :

Code :

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

readfile "PRELUDE.ch".

Edit:
Une chose vraiment pénible c'est l'absence de récursion simultanée, il n'y a même pas un fold2, par conséquent dès qu'on veut par exemple parcourir deux listes (zip, map2,...)

[gasche]

Je viens de regarder le début et effectivement, c'est assez amusant : lire le prélude sans avoir regardé la doc et essayer de comprendre ce qui se passe est un exercice mental qui a son charme.

l'application semble ne pas exister, il n'y a que des fonctions et la juxtaposition c'est la composition de fonction (g f = g ◦ f)

Je ne suis pas convaincu. Dans le "bind" de SF on lit :

Code :

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

1
2
3
def compose_SF{f: A -> SF B, g: B -> SF C}: A -> SF C
    = a => f a ; ss b => g b
    | _ => ff.

C'est effectivement une composition mais j'ai bien l'impression que "a => f a" réalise une application (d'ailleurs c'est un peu curieux, pourquoi ne peuvent-ils pas faire d'eta-réduction ?). C'est peut-être autre chose que je n'ai pas saisi (les fonctions entre { ... } dans le nom ont un statut spécial, et ce sont les seules applicables, peut-être ?).

[SpiceGuid]

Oui, en catégories f; g c'est g ◦ f.
Sinon tu as raison, il y a sans doute toutes les fonctionnalités habituelles, mais pour l'instant je n'ai joué qu'avec les moyens 'élémentaires'.

Quelques exemples.

Un TAD arbres binaires avec quelques fonctions élémentaires :

Code :

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
data tree(A) -> T
  = leaf: 1 -> T
  | node: A * (T * T) -> T.

def tree_size =
  T =>
  {| leaf: () => zero
   | node: (a,n) => succ add n
   |} T.

def tree_depth =
  T =>
  {| leaf: () => zero
   | node: n => succ max n
   |} T.

def tree_rev =
  T =>
  {| leaf: () => leaf
   | node: (a,(l,r)) => node (a,(r,l))
   |} T.

Un type intervalle pour les arbres binaires triés :

Code :

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

1
2
3
4
data tree_order -> T
  = unsorted : 1 -> T 
  | empty: 1 -> T
  | between: nat * nat -> T.

Un prédicat sorted pour arbres binaires :

Code :

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

1
2
3
4
5
6
7
8
9
10
11
12
13
def tree_sorted =
  T =>
  {| leaf: () => empty
   | node: (c,lr) =>
       { (l,empty) => l
       | (empty,r) => r
       | (between(a,b),between(d,e)) =>
           { true  => between(a,e)
           | false => unsorted 
           } and (lt(b,c),lt(c,d))
       | _ => unsorted
       } lr 
   |} T.

Pour le reste des fonctions sur les arbres binaires de recherche on pourra s'inspirer de mon cours OCaml.

Je n'aime pas bien les entiers unaires, des entiers binaires seraient déjà plus agréables à lire.
D'où l'idée d'un type entiers binaires :

Code :

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

1
2
3
4
5
data nat -> T
  = null : 1 -> T
  | unit : 1 -> T
  | zero : T -> T
  | one  : T -> T.

Du fait que chaque constructeur est un morphisme et que la juxtaposition est la composition il n'y pas besoin de parenthèses, ainsi

Code :

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

one zero one null

désignerait le nombre 10 en décimal.

Quelques opérations de base :

Code :

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
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
(* test de parité *)
def even =
  n =>
  {| null: () => true
   | unit: () => false
   | zero: b  => b 
   | one:  b  => b
   |} n.

(* multiplication par 2 *)
def double =
  n =>
  {| null: () => zero null
   | unit: () => one null
   | zero: m => zero m
   | one:  m => one m
   |} n.

(* successeur *)
def succ =
  n =>
  { (m,false) => m
  | (m,true)  => one m
  }
  {| null: () => (unit,false)
   | unit: () => (null,true)
   | zero: (m,true)  => (one m,false)
         | (m,false) => (zero m,false)
   | one:  (m,true)  => (zero m,true)
         | (m,false) => (one m,false)
   |} n.

(* prédécesseur *)
def pred =
  n =>
  { (unit,_) => null 
  | (zero m,_) => m 
  | (m,_) => m
  }
  {| null: () => (unit,true)
   | unit: () => (null,false)
   | zero: (m,true)  => (one m,true)
         | (m,false) => (zero m,false)
   | one:  (m,true)  => (zero m,false)
         | (m,false) => (one m,false)
   |} n.

(* multiplication *)
def mul =
  (a,b) =>
  { (n,_) => n }
  {| null: () => (null,double b)
   | unit: () => (b,double b)
   | zero: (d,c) => (d,double c) 
   | one:  (d,c) => (add(d,c),double c)
   |} a.

Bien sûr il manque encore plein d'opérations, notamment l'addition, le temps de m'habituer à cette récursion simultanée un peu tortueuse...

[SpiceGuid]

Petite explication concernant la récursion simultanée.
Pour réaliser l'addition en base 2 on doit parcourir deux listes de bits, or il est impossible de progresser/itérer sur deux arguments simultanément.
Pour le faire on doit curryfier la récursion sur deux arguments.
On va faire une itération sur le 1ier argument qui renvoie une itération sur le second argument.

Mais comme on a pas le type des fonctions curryfiées A → B → C il faut d'abord l'introduire explicitement :

Code Charity :

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

data A -> arrow(B,C) = fun: A -> B => C.

Contrairement au post précédent, je vais représenter les entiers en base 2 à l'aide d'une liste de bits, ceci afin de pouvoir déplacer un maximum de code trivial dans des fonctions annexes :

Code Charity :

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
def or
  = (false,false) => false
  | _ => true.

def and
  = (true,true) => true
  | _ => false.

def xor
  = (true,false) =>  true
  | (false,true) =>  true
  | _ => false.

def xnor
  = (true,false) =>  false
  | (false,true) =>  false
  | _ => true.

Les deux opérations unitaires sont l'addition sur 1 bit et le calcul de la retenue :

Code Charity :

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

1
2
3
4
5
6
7
8
9
10
11
def addc =
  ((a,b),c) =>
  { true  => xnor(a,b)
  | false => xor(a,b)
  } c.

def carry =
  ((a,b),c) =>
  { true  => or(a,b)
  | false => and(a,b)
  } c.

Pour simplifier au maximum on suppose que les deux entiers à additionner ont le même nombre de bits, ça nous donne le code suivant pour l'addition :

Code Charity :

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

1
2
3
4
5
6
7
8
9
10
11
12
def add
  = (l1, l2) =>
  {(fun: f) => f (false,l2)}
  {| nil : () =>
         (fun: (true,l) => cons(true,l)
         | (false,l) => l
         )
   | cons: (a,(fun: f)) =>
         (fun: (c,nil) => nil
         | (c,cons (b,l))  => cons(addc((a,b),c),f(carry((a,b),c),l))
         )
   |} l1.

Où c désigne la retenue, laquelle retenue n'est pas propagée dans le 'bon' sens
L'addition se fait donc à l'envers du sens de lecture habituel :

Code :

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

1
2
Charity>> add ([true,false],[true,true]).
[false, false, true] : list(bool)

Qui pourra se lire 1 + 3 = 4.

Vu qu'on ne choisi pas le sens dans lequel opère le catamorphisme je ne vois pas d'autre solution que de renverser les arguments, puis d'effectuer l'addition, puis de renverser le résultat pour finir.

[SpiceGuid]

À l'usage j'ai quand même l'impression que le fold est une primitive de "bas niveau".

Je veux dire que ça correspond tout à fait à la définition que je me fais d'un concept minimaliste :

• c'est théoriquement suffisant
• en pratique ça peut devenir tellement laborieux qu'on ne voit pas comment exploiter l'expressivité théorique

Exemple élémentaire, encore plus difficile que l'addition :
comment fusionner deux listes triées à l'aide du fold

À mon avis le simple fait que je doive me poser la question suffit à disqualifier le fold en tant que seule primitive de récursion exposée à l'utilisateur. Ou bien alors il faudrait accompagner le langage d'une documentation qui explore tous les usages habituels au lieu de se contenter d'affirmer qu'on peut tout faire mais sans exposer les moyens pour le faire.
Par exemple, éventuellement, la liste n'est pas un bon TAD pour représenter un ensemble ordonné. Mais alors ça mérite explication. Pourquoi, si c'est le cas, certains TAD qui fonctionnaient bien avec la récursion générale ne fonctionne plus avec le fold ? Il ne faut pas laisser de zone obscure dans laquelle le programmeur pourrait se sentir incompétent (et donc piégé).

[Alp]

Soit dit en passant, ça serait sympa de comparer leur version des tours de Hanoi avec Haskell ou OCaml : ftp://ftp.cpsc.ucalgary.ca/pub/proje.../misc/hanoi.ch