Re: bizarrerie du typage (fwd)

[Pierre Weis <weis>]

From: Didier Rousseau <Didier.Rousseau@cnam.fr>
Message-Id: <199701131435.PAA16829@fermi.cnam.fr>
X-Authentication-Warning: fermi.cnam.fr: localhost [127.0.0.1] didn't use HELO protocol
To: caml-list@inria.fr
Subject: Re: bizarrerie du typage  
In-reply-to: Your message of "Sun, 12 Jan 97 20:19:43 +0100."
             <Pine.GSO.3.95.970112201324.25242B-100000@brotteaux> 
Date: Mon, 13 Jan 97 15:35:36 +0100
X-Mts: smtp

[Note du mode'rateur: Didier a envoye' 2 messages successifs, que j'ai
concate'ne's pour limiter le traffic]

Bonjour a tous

reponse au message de David.Monniaux@ens-lyon.fr

>...
>#let zero = fun x y -> y;;
>val zero : 'a -> 'b -> 'b = <fun>
>#let succ = fun n f x -> n f (f x);;
>val succ : (('a -> 'b) -> 'b -> 'c) -> ('a -> 'b) -> 'a -> 'c = <fun>
>#let un = succ zero;;
>val un : ('_a -> '_b) -> '_a -> '_b = <fun>
>#let deux = succ un;;
>val deux : ('_a -> '_a) -> '_a -> '_a = <fun>
>#deux (fun x -> x) 0;;
>- : int = 0
>#deux;;
>- : (int -> int) -> int -> int = <fun>
>
>Pourquoi le type de "deux" a-t-il change?


il y a une difference entre une variable de type  'a et '_a
l'une est generalisee, tandis que l'autre ne l'est pas encore...
et donc le sera des la premiere utilisation...

De facon generale :

soit une fun  f : 'a -> 'b -> 'b
puis  let f0 = f 0;;

ne sera pas accepte a la compil
le 'b ne pourra pas etre generalise

=> solution : let f0 x = f 0 x;;
=> il faut dans ce cas preciser tous les arguments


Donc en general, il y a un probleme entre variable de type et eta-reduction.

Mais je laisse la parole aux specialistes.

Didier Rousseau

*********************************************************
*       " L'imagination est plus importante             *
*               que la connaissance. "                  *
*                                                       *
*                                       A. E.           *
*********************************************************