Date: Mon, 28 Apr 1997 11:07:27 +0800
From: Sven LUTHER <luther@phivolcs.dost.gov.ph>
To: Caml List <caml-list@inria.fr>
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
This archive was generated by hypermail 2b29 : Sun Jan 02 2000 - 11:58:10 MET