types recursifs ...

types recursifs ...

[Sven LUTHER]

bonjours ...

j'ai quelques petit problemes avec les types recursifs. 

je ne sais pas si cela est la bonne maniere de faire ce que j'ai envie
de faire.

en fait je veut definir des lambda termes definissant des types, et pour
cela je veut separer la partie qui concerne le lambda calcul (
abstraction, variables, application ...) de symboles de types de base.

pour cela j'ai penser que la repartition suivante serait bonne :

	type 'a t = Int | Bool | Arrow of 'a * 'a

	let rec viewt = function
		| Int -> print_string "Int"
		| Bool -> print_string "Bool"
		| Arrow (l, r) -> viewt r; print_string " -> "; viewt l

	type term =
		| V of int
		| S of term t
		| Abs of term

	let rec view = function
		| V (x) -> print_string "V_"; print_int x
		| S (s) -> viewt s				(* probleme 1 *)
		| Abs (l) -> print_string "\\."; view l

	let test = Abs (Arrow (V 1, Int))			(* probleme 2 *)

on devrait donc obtenir la signature suivante :

	type 'a t = | Int | Bool | Arrow of 'a * 'a
	val viewt : ('a t as 'a) -> unit
	type term = | V of int | S of term t | Abs of term
	val view : term -> unit
	val test : term

cependant, pour "viewt s" (probleme 1) on obtient l'erreur suivante :

	This expression has type term t but is here used with type 'a t as 'a

et pour "test" (probleme 2) l'erreur suivante :

	This expression has type 'a t but is here used with type term

il semblerait qu'il y a ici une malfonction dans le typage, a moins que
je n'ai pas entierement compris comment fonctionne les types recursifs.
dans ce cas je m'excuse du derangement.

en effet, le type ('a t as 'a) signifie que le type 'a et le type 'a t
sont identifier, donc 

	pour term t, 'a = term, term = term t = 'a t = 'a ???

apparement le typeur n'arrive pas unifier 'a et term dans ce cas ...

de plus le type de t ne devrait il pas etre ('a t as 'a) des le moment
ou il est definis, et non seuleument plus tard, lorsque l'on s'en sert
dans viewt ?

Amicalement 


Sven LUTHER

Re: types recursifs ...

[Didier Rousseau]

bonjour a tous,

	Sven LUTHER nous a ecrit :

<j'ai quelques petit problemes avec les types recursifs. 
<...
<	type 'a t = Int | Bool | Arrow of 'a * 'a
<
<	let rec viewt = function
<		| Int -> print_string "Int"
<		| Bool -> print_string "Bool"
<		| Arrow (l, r) -> viewt r; print_string " -> "; viewt l
<...


le sens que l'on peut deduit de votre fonction "viewt" ne correspond pas au type 
defini "'a t"
dans le dernier cas de filtrage :
		| Arrow (l, r) -> viewt r; print_string " -> "; viewt l

le typeur deduit que "l" et "r" sont du meme type que l'arg de "viewt" : 'a t
puisque le filtrage porte sur ce type
Or  si par la suite on defini un type "tt" tel que :
	type tt == int t;;

alors Arrow(x,y), de type  int t, ou x et y sont des int


le type recursif que vous auriez du definir etait :
	type 'a t = Int | Bool | Arrow of 'a t * 'a t


mais dans ce cas quel est l'interet du 'a ??



Didier Rousseau
droussea@cnam.fr

Re: types recursifs ...

[Sven LUTHER]

Didier Rousseau wrote:

> le sens que l'on peut deduit de votre fonction "viewt" ne correspond pas au type
> defini "'a t"
> dans le dernier cas de filtrage :
>                 | Arrow (l, r) -> viewt r; print_string " -> "; viewt l
> 
> le typeur deduit que "l" et "r" sont du meme type que l'arg de "viewt" : 'a t
> puisque le filtrage porte sur ce type
> Or  si par la suite on defini un type "tt" tel que :
>         type tt == int t;;
> 
> alors Arrow(x,y), de type  int t, ou x et y sont des int
> 
> le type recursif que vous auriez du definir etait :
>         type 'a t = Int | Bool | Arrow of 'a t * 'a t

Oui je vois ou est mon erreur maintenant, c'est dans la definition de la
fonction viewt
qu'est le probleme.

en fait ce que je voulais faire, c'est etendre le type term par le type
term t. 
je pense donc que je n'ai pas choisi le bon moyen de faire cela.

cependant il me semblait que :

	si ('a t as 'a) designe un type recursif alors 'a et 'a t devrait etre
les memes types

	et donc term t devient (term t as term) et donc term t et term sont les
memes types.

est-ce totalement errone, ai-je mal compris le manuel, ou est-ce
seulement dans la 
definition de la fonction viewt que je m'y suis mal pris.

Sven LUTHER

Re: types recursifs ...

[Didier Rousseau]

Sven LUTHER wrote:

> ...
>	si ('a t as 'a) designe un type recursif alors 'a et 'a t devrait etre
> les memes types
> 
> 	et donc term t devient (term t as term) et donc term t et term sont les
> memes types.
> ...

Prenons un exemple :
le type predefini, list, est equivalent a cette definition :
	type 'a list = [] | :: of 'a*'a list

si l'on utilise ce type avec des "int" : int list
il est claire que "int" et "int list" sont deux types differents !!


> ...
> est-ce totalement errone, ai-je mal compris le manuel, ou est-ce
> seulement dans la 
> definition de la fonction viewt que je m'y suis mal pris.
> ...


le probleme est d'eviter que le typeur deduise de la focntion "viewt" que "l" et "r" de 
Arrow, sont du meme type que l'arg de "viewt" 
par consequent vous ne pouvez pas apeller "viewt" dans le cas Arrow, mais vous devez 
utiliser une autre fonction de type  'a->unit. 2 solutions :

	- soit ajouter un arg a "viewt" :
		let viewt f = function
			| Int -> print_string "Int"
			| Bool -> print_string "Bool"
			| Arrow (l, r) -> f r; print_string " -> "; f l


	- soit ajouter un arg a Arrow :
		type 'a t = Int | Bool | Arrow of ('a->unit) * 'a * 'a

		let viewt = function
			| Int -> print_string "Int"
			| Bool -> print_string "Bool"
			| Arrow (f, l, r) -> f r; print_string " -> "; f l

Prenons cette derniere solution, ce qui donne finalement :
	type 'a t = Int | Bool | Arrow of ('a->unit) * 'a * 'a

	let viewt = function
		| Int -> print_string "Int"
		| Bool -> print_string "Bool"
		| Arrow (f, l, r) -> f r; print_string " -> "; f l

	type term =
		| V of int
		| S of term t
		| Abs of term

	let rec view = function
		| V (x) -> print_string "V_"; print_int x
		| S (s) -> viewt s
		| Abs (l) -> print_string "\\."; view l

	let test = Abs (S (Arrow (view, V 1, S Int)))


ou un peu plus general :
	type 'a t = Int | Bool | Arrow of ('a->unit) * 'a * 'a

	let viewt = function
		| Int -> print_string "Int"
		| Bool -> print_string "Bool"
		| Arrow (f, l, r) -> f r; print_string " -> "; f l

	type 'a term =
		| V of int
		| S of 'a t
		| Abs of 'a term

	let rec view = function
		| V (x) -> print_string "V_"; print_int x
		| S (s) -> viewt s
		| Abs (l) -> print_string "\\."; view l

	let test1 = Abs (S (Arrow (view, V 1, S Int)))
	let test2 = Abs (S (Arrow (viewt, Int,Bool)))
------------------------------------------------------------

Didier Rousseau

Re: types recursifs ...

[Sven LUTHER]

Didier Rousseau wrote:
> 
> Sven LUTHER wrote:
> 
> > ...
> >       si ('a t as 'a) designe un type recursif alors 'a et 'a t devrait etre
> > les memes types
> >
> >       et donc term t devient (term t as term) et donc term t et term sont les
> > memes types.
> > ...
> 
> Prenons un exemple :
> le type predefini, list, est equivalent a cette definition :
>         type 'a list = [] | :: of 'a*'a list
> 
> si l'on utilise ce type avec des "int" : int list
> il est claire que "int" et "int list" sont deux types differents !!
> 

En fait ce que je voulais c'est bel et bien definir un type recursif,
c'est a dire du type :

'a t as 'a, ou peut etre 'a list as 'a.

cela est-il possible en Caml ?

d'apres la discution sur ce sujet, je ne pense pas que ce soit possible.

y a-t-il un autre mecanisme pour etendre un type, voir un module, un peu
a la facon
de l'heritage pour les objets, quelque choses qui permettrait d'etendre
un type ou un
module, eventuellement dynamiquement ?

Sven LUTHER

Re: types recursifs ...

[Emmanuel Engel]

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

[LONG] Re: types recursifs ...

[Christian Boos]

[long french version below, with code examples]

Hello,

  I would first reply to Sven that recursive types are allowed in the O'Caml
langage, under some conditions. Let's quote the manual : 

| Recursive types
|
| The type expression typexpr as ' ident denotes the same type as typexpr,
| and also binds the type variable ident to type typexpr both in typexpr and
| in the remaining part of the type. If the type variable ident actually
| occurs in typexpr, a recursive type is created. Recursive types are allowed
| as long as any recursion crosses a type constructor or an object type.
|                                   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

In the french version below, I also give 2 small & useless examples...


  Next, Sven asked about module and type extension possibilities.
There is a little support for that: the 'include' keyword which can be 
used to include a signature inside another. 
Then, why is there no 'include' for structure definitions ?

This topic suggested me to bring back the hotly debatted concept of 
dynamic structure creation... see the forthcoming mail!



==================================================================

Sven LUTHER writes:
 > Didier Rousseau wrote:
 > > ...
 > > Sven LUTHER wrote:
 > > > ...
 > > > si ('a t as 'a) designe un type recursif alors 'a et 'a t devrait etre
 > > > les memes types
 >
 > En fait ce que je voulais c'est bel et bien definir un type recursif,
 > c'est a dire du type :
 >
 > 'a t as 'a, ou peut etre 'a list as 'a.
 >
 > cela est-il possible en Caml ?
 >
 > d'apres la discution sur ce sujet, je ne pense pas que ce soit possible.
 >

Si, c'est possible, mais il faut passer par l'utilisation d'un constructeur,
ou bien utiliser une classe, comme indique dans la doc (htmlman/node5.5.html),
que je me permets de citer :

| Recursive types
|
| The type expression typexpr as ' ident denotes the same type as typexpr,
| and also binds the type variable ident to type typexpr both in typexpr and
| in the remaining part of the type. If the type variable ident actually
| occurs in typexpr, a recursive type is created. Recursive types are allowed
| as long as any recursion crosses a type constructor or an object type.
|                                   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Les types recursifs sont interessants pour construire des fonctions
"autoregeneratrices" (si je ne m'abuse cela correspond a du "continuation-
passing style").

Exemple :

| type 'a generator = G of 'a * (unit -> 'a generator)
|
| # let gen t =
|   let last = pred (Array.length t) in
|   let rec forward i () =
|     let i', dir =
|       if i < last then (succ i, forward) else (pred i, backward)
|     in
|     G (t.(i'), dir i')
|   and backward i () =
|     let i', dir =
|       if i > 0 then (pred i, backward) else (succ i, forward)
|     in
|     G (t.(i'), backward i')
|   in
|   (G (t.(0), forward 0))
|
|
| let next (G (v, g)) = (v, g ())
| ;;
| val gen : 'a array -> 'a generator = <fun>
| val next : 'a generator -> 'a * 'a generator = <fun>
| # let g = gen [| 0; 1; 2 |];;
| val g : int generator = G (0, <fun>)
| # let (v, g) = next g;;
| val v : int = 0
| val g : int generator = G (1, <fun>)
| # let (v, g) = next g;;
| val v : int = 1
| val g : int generator = G (2, <fun>)
| # let (v, g) = next g;;
| val v : int = 2
| val g : int generator = G (1, <fun>)
| # let (v, g) = next g;;
| val v : int = 1
| val g : int generator = G (0, <fun>)
| # let (v, g) = next g;;
| val v : int = 0
| val g : int generator = G (1, <fun>)
| # let (v, g) = next g;;
| val v : int = 1
| val g : int generator = G (0, <fun>)
| #

On peut bien sur trouver des exemples plus utiles (mais certainement
plus longs !).

Encore un autre, le combinateur Y :

en SML: (issu de la comp.lang.ml FAQ)

| datatype 'a t = T of 'a t -> 'a
|
|  val y = fn f => (fn (T x) => (f (fn a => x (T x) a)))
|                  (T (fn (T x) => (f (fn a => x (T x) a))))

en O'Caml (ou en Caml-Light):

| # type 'a t = T of ('a t -> 'a);;
| type 'a t = | T of ('a t -> 'a)
|
| # let y f = let g (T x) = f (fun a -> x (T x) a) in g (T g);;
| val y : (('a -> 'b) -> 'a -> 'b) -> 'a -> 'b = <fun>
|
| # y (fun f a -> if a = 0 then 1 else f (pred a) * a) 5;;
| - : int = 120
|
| # let map g = y (fun f a -> match a with [] -> [] | h::t -> g h :: f t);;
| val map : ('a -> 'b) -> 'a list -> 'b list = <fun>


------------------------------------------------------------------

 > y a-t-il un autre mecanisme pour etendre un type, voir un module, un peu
 > a la facon
 > de l'heritage pour les objets, quelque choses qui permettrait d'etendre
 > un type ou un
 > module, eventuellement dynamiquement ?

Pour etendre un module, ou au moins son type, il y a le fameux
"include MODULE_TYPE", non documente. Il en a ete fait mention lors de
discussions precedentes sur cette liste
(cf. http://pauillac.inria.fr/caml/caml-list/0602.html )
Il permet de definir un nouveau type de module en realisant simplement
l'inclusion textuelle de la specification d'un autre type de module.

Par contre, pour definir l'implementation, il n'y a rien de tel : on est
oblige de redefinir toutes les valeurs :

On a par exemple :

| # module type A_t = sig val a : int end;;
| module type A_t = sig val a : int end
| # module type Aext_t = sig include A_t val b : int end;;
| module type Aext_t = sig val a : int val b : int end

Mais :

| module A = struct let a  = 1 end;;
| module A : sig val a : int end
| # module Aext = include A let b = 1 end;;
| Characters 14-21:
| Syntax error

obligeant a ecrire :

| # module Aext = struct let a = A.a let b = 2 end;;
| module Aext : sig val a : int val b : int end

Pourquoi pas un 'include' pour l'implementation ?
Il serait toujours possible de redefinir certaines valeurs apres
l'inclusion.

Pour etendre un module dynamiquement ... c'est une autre histoire.
A l'heure actuelle, il n'y a meme aucune possibilite d'instancier
dynamiquement des modules, ce qui est bien dommage.

A ce sujet, voir mon prochain mail ...


-- Christian 

Re: types recursifs ...

[Jerome Vouillon]

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