Re: types recursifs ...

From: Emmanuel Engel (Emmanuel.Engel@lri.fr)
Date: Wed May 14 1997 - 10:39:13 MET DST


Date: Wed, 14 May 1997 10:39:13 +0200
From: Emmanuel Engel <Emmanuel.Engel@lri.fr>
To: Sven LUTHER <luther@phivolcs.dost.gov.ph>
Subject: Re: types recursifs ...

Je ne sait pas tres bien ce que vous entendez par type recursif.
Si le probleme est de definir un type 'a t tel que 'a t = 'a ce
n'est pas difficile en objective caml:

~> ocaml
        Objective Caml version 1.05
# type 'a t = Leaf of 'a | Node of ('b t as 'b) * ('c t as 'c);;
type 'a t = | Leaf of 'a | Node of 'a * 'a constraint 'a = 'a t

On peut definir des valeurs et des fonctions qui ont ce type.

# let rec t1 = Leaf t1 ;;
val t1 : 'a t as 'a =
  Leaf
   (Leaf
     (Leaf
       (Leaf
         (Leaf
           (Leaf
             (Leaf
               (Leaf
                 (Leaf
                   (Leaf
                     (Leaf
                       (Leaf
                         (Leaf
                           (Leaf
                             (Leaf
                               (Leaf
                                 (Leaf
                                   (Leaf
                                     (Leaf
                                       (Leaf
                                         (Leaf
                                           (Leaf
                                             (Leaf
                                               (Leaf
                                                 (Leaf
                                                   (Leaf
                                                     (Leaf
                                                       (Leaf
                                                         (Leaf
                                                           (Leaf (Leaf
.))))))))))))))))))))))))))))))
# let rec t2 = Node (t2,t2);;
val t2 : 'a t as 'a =
  Node
   (Node
     (Node
       (Node
         (Node
           (Node
             (Node
               (Node
                 (Node
                   (Node
                     (Node
                       (Node
                         (Node (Node (Node (Node ., ...), ...), ...),
...),
                        ...),
                      ...),
                    ...),
                  ...),
                ...),
              ...),
            ...),
          ...),
        ...),
      ...),
    ...)

# let rec iter f = function
    Leaf t -> f t
   |Node(t1,t2) -> f t1; f t2;;
val iter : (('a t as 'a) -> 'b) -> ('c t as 'c) t -> 'b = <fun>
# let rec fold f accu = function
    Leaf t -> f accu t
   |Node(t1,t2) -> f (fold f accu t1) t2;;
val fold : ('a -> ('b t as 'b) -> 'a) -> 'a -> ('c t as 'c) -> 'a =
<fun>

On peut remarquer qu'il n'est pas indispensable de definir un type
avec une contrainte 'a t as t pour obtenir des valeurs qui aient un type
avec de telles contraintes:

# let rec l = l :: l;;
val l : 'a list as 'a =
  [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[.; ...]; ...]; ...]; ...]; ...]; ...];
...];
                          ...];
                         ...];
                        ...];
                       ...];
                      ...];
                     ...];
                    ...];
                   ...];
                  ...];
                 ...];
                ...];
               ...];
              ...];
             ...];
            ...];
           ...];
          ...];
         ...];
        ...];
       ...];
      ...];
     ...];
    ...];
   ...]

L'interet de tels types me m'apparais pas de facon immediate. Je ne vois
pas de facon de definir des valeurs avec un tel type qui ne soient pas
un cas terminal (ie la liste vide par exemple) ou un terme infini; les
contraintes du langage impose alors que le terme presente une regularite
certaine: cela ne peut etre qu'une definition syntaxique et pas le
resultat
d'un (vrai) calcul.

Une seconde curiosite avec les types recursif est la possibilite de
definir
un type avec une recursion non triviale (ie non monomorphe).
c'etait possible dans CAML.

~> caml
   CAML (sun4) (V3.1.2) by INRIA Thu Feb 4

#type 'a term =
# Leaf of 'a
# |Node of ('a * 'a) term ;;
Type term is defined

Le definition de valeurs de ce type ne pose alors pas de probleme

#let t = Node(Node(Leaf((1,2),(3,4))));;
Value t is (Node (Node (Leaf ((1,2),3,4)))) : int term

pas plus que de fonctions pour ces termes

#let rec map f = function
# Leaf t -> Leaf (f t)
# |Node t-> Node(map (fun (x,y)->f x,f y) t);;
Value map is <fun> : ('a -> 'b) -> 'a term -> 'b term

par contre le typage deviens difficile, la fonction map
est utilisee de facon polymorphe dans sa definition.

 

Emmanuel Engel

-- 

- Emmanuel Engel



This archive was generated by hypermail 2b29 : Sun Jan 02 2000 - 11:58:10 MET