Message-Id: <9210071731.AA23910@concorde.inria.fr>
Date: Wed, 7 Oct 92 18:31:19 FST
From: "Claude Fleurey" <FLEUREY@ESONVM2.VNET.IBM.COM>
To: caml-list@margaux
Subject: compr'hension des m'canismes de base.
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
----------------------------------------------------------------------------
]