types recursifs ...

From: Sven LUTHER (luther@phivolcs.dost.gov.ph)
Date: Mon Apr 28 1997 - 05:07:27 MET DST


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