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 UAA11845 for caml-redistribution; Thu, 15 May 1997 20:02:54 +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 TAA11468 for <caml-list@pauillac.inria.fr>; Thu, 15 May 1997 19:30:59 +0200 (MET DST)
Received: from nef.ens.fr (nef.ens.fr [129.199.96.12]) by nez-perce.inria.fr (8.8.5/8.7.3) with ESMTP id TAA12378 for <caml-list@inria.fr>; Thu, 15 May 1997 19:30:56 +0200 (MET DST)
Received: from nave.ens.fr (nave.ens.fr [129.199.130.3])
          by nef.ens.fr (8.8.5/jtpda-5.1) with ESMTP id TAA26226
          for <caml-list@inria.fr>; Thu, 15 May 1997 19:30:54 +0200 (MET DST)
Received: from localhost (vouillon@localhost) by nave.ens.fr (8.8.5/jb-1.1)
	id TAA22068 for <caml-list@inria.fr>; Thu, 15 May 1997 19:30:53 +0200 (MET DST)
X-Authentication-Warning: nave.ens.fr: vouillon owned process doing -bs
Date: Thu, 15 May 1997 19:30:52 +0200 (MET DST)
From: Jerome Vouillon <vouillon@clipper.ens.fr>
X-Sender: vouillon@nave
Reply-To: Jerome Vouillon <vouillon@clipper.ens.fr>
To: Caml List <caml-list@inria.fr>
Subject: Re: types recursifs ...
In-Reply-To: <33797A31.4765@lri.fr>
Message-ID: <Pine.SUN.3.95.970515185203.22011A-100000@nave>
MIME-Version: 1.0
Content-Type: TEXT/PLAIN; charset=US-ASCII
Sender: weis



On Wed, 14 May 1997, Emmanuel Engel wrote:

> ~> 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
[...]
> # 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.

Voici un exemple.

  # type 'a t = | A | B of 'a;;
  type 'a t = | A | B of 'a
  # let x = B(1, B (2, A));;
  x : (int * (int * 'a t) t) t = B (1, B (2, A))

Il n'y a pas de recursion dans le type infere pour x. Mais on peut
donner a x un type recursif.

  # (x : (int * 'a) t as 'a);;
  - : (int * 'a) t as 'a = B (1, B (2, A))

Une fonction iterant sur de telles listes aura un type recursif.

  # let rec iter f = function A -> () | B (x, l) -> f x; iter f l;;
  val iter : ('a -> 'b) -> (('a * 'c) t as 'c) -> unit = <fun>

En fait, on definit plutot t par

  # type 'a t = | A | B of 'a * 'a t;;

On n'a plus alors besoin de type (explicitement) recursif pour typer
les examples precedents. La recursion est masquee par le constructeur
de type B.

  # let x = B(1, B (2, A));;
  val x : int t = B (1, B (2, A))
  # let rec iter f = function A -> () | B (x, l) -> f x; iter f l;;
  val iter : ('a -> 'b) -> 'a t -> unit = <fun>

En pratique, lorsque le type infere' pour une expression est recursif,
c'est qu'il y a en fait une erreur dans la definition de cette
expression. Ce genre de resultat etant tres deconcertant la premiere
fois que l'on tombe dessus, la recursion ne sera a priori acceptee
dans la prochaine release de ocaml que la` ou` elle est vraiment
necessaire (c'est-a-dire lorsqu'elle traverse un objet; par exemple : 
<x : 'a> as 'a).  Il est de toute facon toujours possible de masquer
la recursion en utilisant des types construits (voir le mail de
Christian Boos).

-- Jerome Vouillon