Version française
Home     About     Download     Resources     Contact us    
Browse thread
types recursifs ...
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: Didier Rousseau <Didier.Rousseau@c...>
Subject: Re: types recursifs ...

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