bizarrerie du typage

bizarrerie du typage

[David Monniaux]

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>

Pourquoi le type de "deux" a-t-il changé?
(cela fait aussi avec la version 1.03)

N'aurais-je rien compris au système de typage du CAML?
Il me semblait pourtant que quand un identificateur était lié à un terme
déjà typé, son type était bien établi (égal à celui de ce terme), et ne
changeait pas...

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

Re: bizarrerie du typage

[Eric HASSOLD]

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