compr'hension des m'canismes de base.

compr'hension des m'canismes de base.

[Claude Fleurey]

   Mon intervention refle`te sans doute une me'connaissance des me'canismes
   de base qui s'appliquent aux langages fonctionnels (re'duction des
   termes).

   Etant donne'e une abstraction
         fun x y z -> x y z
   je pensais que l'e'valuation de
         (fun x y z -> x y z) alpha1 alpha2 alpha3
   devait rendre le meme re'sultat que l'e'valuation de
         (alpha1 alpha2 alpha3).

   Dans l'exemple suivant ce principe ne semble pas s'appliquer:
   Pourquoi ce terme est-il rejete' (au moment ou` 'trois' est passe')
  #(fun nb f x -> nb f (nb (fun u v -> v) f x)) trois inc 0 ;;
   et celui-ci accepte'  ?
  #(trois inc (trois (fun u v -> v) inc 0)) ;;

   Ou encore pourquoi (fn2 trois inc 0) est-il rejete' au moment du typage
   alors que ins2 est accepte' (et donne le re'sultat attendu) ?

   Merci pour votre aide (et votre indulgence).

    Claude Fleurey

>       Caml Light version 0.5

#let trois = fun x y -> x (x (x y)) ;;
trois : ('a -> 'a) -> 'a -> 'a = <fun>
#let inc   = fun x -> x + 1 ;;
inc : int -> int = <fun>

#let fn2  = fun nb f x -> nb f (nb (fun u v -> v) f x) ;;
fn2 : (('a -> 'b -> 'b) -> ('a -> 'b -> 'b) -> 'c -> 'a -> 'b -> 'b) -> ('a -> 'b -> 'b) -> 'c -> 'c -> 'a -> 'b -> 'b = <fun>

#let ins2 = trois inc (trois (fun u v -> v) inc 0) ;;
ins2 : int = 3

#fn2 trois inc 0 ;;
> Toplevel input:
>fn2 trois inc 0 ;;
>    ^^^^^
> Expression of type (('a -> 'a) -> 'a -> 'a) -> ('a -> 'a) -> 'a -> 'a
> cannot be used with type (('a -> 'a) -> 'a -> 'a) -> (('a -> 'a) -> 'a -> 'a) -> 'b -> ('a -> 'a) -> 'a -> 'a

[Note du mode'rateur:

 Vous confondez e'valuation et typage
 (fun x y z -> x y z) alpha1 alpha2 alpha3
 et alpha1 alpha2 alpha3
 sont des applications: l'ordre d'e'valuation des arguments n'est pas
 garanti en Caml donc rien n'impose d'obtenir le me^me re'sultat si
 alpha1 alpha2 alpha3 font des effets de bords (affectations ou`
 lecture/e'criture sur fichier). Les deux expressions
 sont en revanche e'quivalentes si alpha1 alpha2 alpha3 sont des
 expressions pures.

 Sur le plan typage elles sont e'galement e'quivalentes (elles sont ou
 bien typables avec le me^me type, ou bien non typables).

 Cette proprie'te' est parfaitement vraie pour la fonction
 (fun x y z -> x y z). Cependant votre exemple (fn2) n'est pas exactement
 celui-la`! Or il n'est pas vrai en ge'ne'ral que l'application
 (fun x y z -> body) E1 E2 E3 soit e'quivalente (pour le typage) a`
 body (ou` x est remplace' par E1, y par E2 et z par E3 avec les
       pre'cautions d'usage)
 Donc une petite modification de la fonction (fun x y z -> x y z)
 peut rendre cette e'quivalence fausse: il suffit pour cela de faire
 intervenir le polymorphisme, donc d'employer un identificateur avec 2
 types incompatibles, donc de faire apparai^tre 2 occurrences du me^me
 identificateur dans le corps de l'abstraction.
 Par exemple (si I est l'identite' (fun x -> x))

 I I est bien type' alors que (fun x -> x x) I est mal type'.

 Rappelons en effet que les ARGUMENTS d'une fonction doivent avoir
 exactement le ME^ME TYPE dans tout le corps de la fonction, et que
 l'e'galite' se'mantique let x = E1 in E2 == (fun x -> E2) E1 n'est
 pas ve'rifie'e par le ve'rificateur de type, qui introduit du
 polymorphisme dans la premie`re forme et pas dans la seconde.
 
 C'est ce phe'nome`ne qui vous arrive puisque vous utilisez 2 fois f et
 2 fois nb dans le corps de fn2.

 Ainsi fn2 trois inc 0 est mal type' mais est e'quivalent (recopie du
 corps de fn2) a`

 (fun nb f x -> nb f (nb (fun u v -> v) f x)) trois inc 0

 Si l'on re'e'crit le be'ta-redex (l'application) a` l'aide d'un let
 on obtient la phrase bien type'e suivante

#let nb,f,x = trois,inc,0 in nb f (nb (fun u v -> v) f x);;
3 : int

 Gra^ce a` la construction let l'identificateur nb a e'te' type' de
 deux facons diffe'rentes dans l'expression
 nb f (nb (fun u v -> v) f x)

 Le me^me phe'nome`ne (a` l'envers) prouve que fn2 ne peut pas
 s'appliquer a` inc puisque:

#let fn2  = fun nb (f:int -> int) x -> nb f (nb (fun u v -> v) f x) ;;
> Toplevel input:
>let fn2  = fun nb (f:int -> int) x -> nb f (nb (fun u v -> v) f x) ;;
>                                                ^^^^^^^^^^^^
> Expression of type 'a -> 'b
> cannot be used with type int

 Retenons qu'on ne peut pas employer un argument de fonction de facon
 polymorphe dans le corps de la fonction en particulier parcequ'on ne
 peut pas exprimer le type qu'aurait la fonction dans le syste`me de
 type de ML, pour lequel tous les types polymorphes sont toujours quantifie's
 universellement en te^te (de facon pre'nexe):
 (pour tout type 'a, 'b, ...) expression de type.

 On peut donc e'crire
 let I = fun x -> x in
 I "ok", I true

 Mais pas la fonction
 let apply_string_bool f = f "ok", f true;;
 car cette fonction ne devrait s'appliquer qu'a` des arguments
 polymorphes, et devrait donc avoir un type du genre
 (forall 'b.  (for all 'a. 'a -> 'b) -> ('b * 'b))
 qui n'est pas quantifie' de facon pre'nexe.

 Finalement il faut savoir que toute lambda expression n'est pas
 typable en ML, ni me^me e'valuable puisque ML a une strate'gie
 d'e'valuation en appel par valeur sans e'valuation dans le corps des
 fonctions (be'ta-re'duction faible en appel par valeurs) mais qu'en
 revanche il est tre`s facile d'e'crire en ML un e'valuateur ge'ne'ral du
 lambda-calcul (de'crit comme un type de donne'es ML) qui mettra bien
 en e'vidence les choix de strate'gie de re'duction et pourra e'valuer
 ``sous les lambdas'' c'est-a`-dire dans le corps des fonctions.
 C'est un bon exercice pe'dagogique! 

Pierre Weis
----------------------------------------------------------------------------
Formel Project
INRIA, BP 105, F-78153 Le Chesnay Cedex (France)
E-mail: Pierre.Weis@inria.fr
Telephone: +33 1 39 63 55 98
----------------------------------------------------------------------------
]