Re: bizarrerie du typage

[Eric HASSOLD <hassold@mad.unice.fr>]

David Monniaux wrote:
> 
> J'ai un exemple assez amusant de bizarreries du typage:
> 
>         Objective Caml version 1.01
> 
> #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>
> 
le symbole _ dans le type ('_a et non 'a) indique qu'il s'agit d'un type
statique qui doit cependant attendre le premier appel de la fonction
pour etre resolu et assigne definitivement (le type int dans ton 
exemple).
Si tu veux preserver le polymorphisme des fonctions un et deux, declare
les arguments explicitement, c-a-d

let un = fun f x -> succ zero f x;;
val un : ('a -> 'b) -> 'a -> 'b = <fun>

let deux = fun f x -> succ un f x;;
val deux : ('a -> 'a) -> 'a -> 'a = <fun>

Alors, tu obtiens bien :

deux (fun x -> x) 0;;
- : int = 0

mais toujours

deux;;
- : ('a -> 'a) -> 'a -> 'a = <fun>

> "Si l'informatique marchait, cela se saurait."

Je trouve que ca se sait...

----- 
Eric Hassold
Université de Nice - Sophia Antipolis
Laboratoire de Mathématiques
Parc Valrose
06108 Nice Cedex 02 - France

Téléphone : (33) 04 92 07 62 89
Email     : hassold@mad.unice.fr
WWW       : http://math.unice.fr/~hassold