Re: types recursifs ...

From: Didier Rousseau (Didier.Rousseau@cnam.fr)
Date: Wed Apr 30 1997 - 14:42:07 MET DST


From: Didier Rousseau <Didier.Rousseau@cnam.fr>
Message-Id: <199704301242.OAA00827@fermi.cnam.fr>
To: luther@phivolcs.dost.gov.ph
Subject: Re: types recursifs ...
Date: Wed, 30 Apr 97 14:42:07 +0200

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



This archive was generated by hypermail 2b29 : Sun Jan 02 2000 - 11:58:10 MET