From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: weis
Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id SAA18803 for caml-redistribution; Wed, 14 May 1997 18:09:21 +0200 (MET DST)
Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id KAA09867 for <caml-list@pauillac.inria.fr>; Wed, 14 May 1997 10:39:07 +0200 (MET DST)
Received: from lri.lri.fr (root@lri.lri.fr [129.175.15.1]) by nez-perce.inria.fr (8.8.5/8.7.3) with ESMTP id KAA20212 for <caml-list@inria.fr>; Wed, 14 May 1997 10:39:05 +0200 (MET DST)
Received: from newsun8.lri.fr (newsun8.lri.fr [129.175.8.15])
          by lri.lri.fr (8.8.5/jtpda-5.2) with ESMTP id KAA02723
          ; Wed, 14 May 1997 10:39:04 +0200 (MET DST)
Received: from newsun8 by newsun8.lri.fr
	(8.8.4/local) with SMTP id KAA16360
	; Wed, 14 May 1997 10:39:14 +0200 (MET DST)
Message-ID: <33797A31.4765@lri.fr>
Date: Wed, 14 May 1997 10:39:13 +0200
From: Emmanuel Engel <Emmanuel.Engel@lri.fr>
X-Mailer: Mozilla 3.01Gold (X11; I; SunOS 5.5 sun4m)
MIME-Version: 1.0
To: Sven LUTHER <luther@phivolcs.dost.gov.ph>
CC: Caml List <caml-list@inria.fr>
Subject: Re: types recursifs ...
References: <199704301242.OAA00827@fermi.cnam.fr> <33795E2D.7993B0CA@phivolcs.dost.gov.ph>
Content-Type: text/plain; charset=us-ascii
Content-Transfer-Encoding: 7bit
Sender: weis

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