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