Browse thread
types recursifs ...
[
Home
]
[ Index:
by date
|
by threads
]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: | 1997-04-29 (07:07) |
From: | Sven LUTHER <luther@p...> |
Subject: | types recursifs ... |
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