Re: types recursifs ...

[Jerome Vouillon <vouillon@clipper.ens.fr>]

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