Possible bug report in CAML Light V0.5

Possible bug report in CAML Light V0.5

[(Claude Diderich)]

Bonjour les chercheurs de l'INRIA,

D'abord j'aimerai vous f'eliciter pour votre impl'ementation CAML-Light.
Je la trouve superbe, notamment qu'elle marche sur PC et Mac.

J'ai une question: En ce qui conerne la documentation - Est-ce qu'elle
est disponible en imprim'e (rapport INRIA)? Quels sont les prix et
est-ce qu'on peut commander via e-mail?

Ensuite j'ai eu un probl`eme avec CAML-Light 0.5. Je ne sais pas s'il
s'agit d'une erreur (bug) ou simplement d'une limitation. Voici le probl`eme.
J'aimerai d'eterminer le type de la lambda-expression suivante (cette
expression est due `a Marc Gengler, EPFL/DI-LITH).

fun a -> ((fun x -> (x (x (fun y -> (fun z -> (y (a z)))))))
    (fun u -> ((fun v -> (v (v (fun w -> w)))) (fun t -> (u (u t))))));;

Si je la fais 'evaluer sur une Sun Sparc 2 avec CAML V3.1 (la grosse b'ecane)
j'obtient le r'esultat correct suivant:

   CAML (sun4) (V3.1.1) by INRIA Tue Jun 30

#fun a -> ((fun x -> (x (x (fun y -> (fun z -> (y (a z)))))))
#    (fun u -> ((fun v -> (v (v (fun w -> w)))) (fun t -> (u (u t))))));;
<fun> : (('a -> 'a) -> 'a -> 'a) -> 'a -> 'a

Par contre sous CAML-Light, j'obtiens le message d'erreur suivant:

>       Caml Light version 0.5

#fun a -> ((fun x -> (x (x (fun y -> (fun z -> (y (a z)))))))
    (fun u -> ((fun v -> (v (v (fun w -> w)))) (fun t -> (u (u t))))));;
> Toplevel input:
>    (fun u -> ((fun v -> (v (v (fun w -> w)))) (fun t -> (u (u t))))));;
>                                                          ^
> Expression of type ('a -> 'b) -> 'a -> 'b
> cannot be used with type ('a -> 'b) -> ('a -> 'b) -> 'a -> 'b

En esp'erant que cette information puisse vous ^etre utile, je vous prie
de bien vouloir agr'er l'expression de mes sentiments les meilleurs.

Claude G. Diderich


P.S. Pour mon examen th'eorique de dipl^ome j'ai r'dig'e un rapport
sur CAML (voir en annexe). Si ,ca vous int'eresse, je me freai un plaisir de
vous envoyer une copie.
-----------------------------------------------------------------------------
Claude G. Diderich                              Internet: diderich@di.epfl.ch
30, Avenue S. Reymondin - CH-1009 Pully (VD) - Switzerland - Europe

``Imagination is more important than knowledge''              Albert Einstein
-----------------------------------------------------------------------------

TITRE:	Programmation Fonctionnelle en CAML
AUTEUR:	Claude G. Diderich
	30, Avenue S. Reymondin
	CH-1009 Pully
RESUME':
	Le langage CAML est un langage fonctionnel utilisant le syst`eme de
	typage d'evelopp'e par Robin Milner. Les id'ees de bases de la
	programmation fonctionnelle sont d'ecrites dans cet article. Un bref
	aper,cu historique montre l''evolution des langages fonctionnels.
	Les concepts du langage CAML, comme l'application, l'abstraction, la
	d'efinition de fonctions, les types et autres sont pr'esent'es et
	illustr'es `a l'aide d'exemples. A travers la r'esolution de
	probl`emes classiques, la puissance d'expression du langage est
	montr'ee. Un interpr`ete complet du lambda-calcul a 'et'e impl'ement'e.
	En fin de compte, quelques particularit'es du langage CAML, comme la
	d'efinition de types paresseux ou la d'eclaration de grammaires du
	genre de celles utilis'ee par Yacc, sont d'ecrites.

CAT'EGORIES CR:
	D.1.1 [Techniques de programmation]: Programmation (applicative)
	fonctionnelle; D.3.1 [Langages de programmation]: D'efinitions
	formelles et th'eorie --- syntaxe, s'emantique

MOTS CLEF:
	CAML, Evaluation paresseuse, Fonctions, Inf'erence de types,
	Lambda-calcul, Point fixe, Polymorphisme, Programmation
	fonctionnelle, Types

[Note du mode'rateur:

  Proble`me de typage:
  --------------------
  En ce qui concerne votre exemple il est normal qu'il ne passe pas en
 Caml Light qui imple'mente strictement le typage polymorphe a` la
 Dalmas-Milner. Ceci signifie en particulier que seule la construction
 let introduit du polymorphisme. Or l'application d'une fonction
 imme'diate (une lambda-expression) a` un argument est se'mantiquement
 e'quivalente a` un let:
 (fun x -> in_part) be_part est e'quivalent se'mantiquement a`
 let x = be_part in in_part

  Cette traduction est utilise'e dans le contro^leur de type de Caml
 pour typer
 (fun x -> in_part) be_part comme si l'utilisateur avait tape'
 let x = be_part in in_part.
  Cependant cette dernie`re forme introduit du polymorphisme: x peut
 e^tre utilise' avec plusieurs types diffe'rents dans in_part ce qui
 est interdit par la premie`re forme. Un exemple plus simple de ce
 phe'nome`ne est (fun x -> x x) (fun x -> x) qui est bien type' et rend
 l'identite' en CAML mais est mal type' en Caml Light.

 Votre exemple reproduit 2 fois ce phe'nome`ne puisqu'il est
 e'quivalent a`:
 fun a ->
  let x u = let v t = u (u t) in v (v (fun w -> w)) in
   x (x (fun y z -> y (a z)))

 En effet, si l'on soumet cette dernie`re forme a` Caml Light:
 >       Caml Light version 0.5

 #fun a ->
  let x u = let v t = u (u t) in v (v (fun w -> w)) in
   x (x (fun y z -> y (a z)));;
 - : (('a -> 'a) -> 'a -> 'a) -> 'a -> 'a = <fun>
 #

  Il y a en outre beaucoup de constructions pour lesquelles le typage
 de Caml s'e'loigne du strict typage a la Dalmas-Milner. Vous trouverez
 donc facilement des phrases typables en Caml et non typables en Caml
 Light. L'inverse est vrai aussi, particulie`rement en ce qui concerne
 les valeurs mutables. La seule propriete' assure'e par les deux
 imple'mentations est qu'une phrase bien type'e ne produira pas
 d'erreurs pendant l'exe'cution.

 Documentation:
 -------------
 La documentation Caml Light est toujours accessible par ftp anonyme
 sur ftp.inria.fr (128.93.1.26) dans le directory lang/caml-light/cl5doc*
 En outre je vous rappelle que vous pouvez commander moyennant la
 somme modique de 120F en renvoyant le bon de commande ci-dessous:
    Bon de commande du logiciel CAML-Light ou de sa documentation
    A` retourner a`:

    INRIA  --- SEDIS-Diffusion
    B.P. 105 --- 78153 Le Chesnay Cedex (France)
    Te'l. (33) (1) 39 63 56 27

    Le logiciel CAML-Light et sa documentation sont distribue's pour
    machines Macintosh et PC.

    - Pour le Macintosh, le logiciel est distribue' sur une disquette
    800 Ko, et ne'cessite  2Mo de me'moire vive au minimum, et syste`me 6 ou
    7.
    - Pour compatibles PC, le logiciel est distribue' au choix sur
    disquette 5.25'' (haute densite', 1.2 Mo) ou 3.5'' (haute densite', 1.44
    Mo).  Vous pouvez e'galement de'clarer que l'un ou l'autre format vous
    convient indiffe'remment. Il ne'cessite 640 Ko de me'moire vive au
    minimum, MS-DOS version 3.3 ou suivantes, un lecteur de disquettes
    haute densite' 3.5'' ou 5.25''.

    Cochez une et une seule case parmi:
     _
    |_| Documentation seule (sans le logiciel).
     _
    |_| Documentation plus disquette pour le Macintosh.
     _
    |_| Documentation plus disquette pour le PC.
        Disquette format 5.25'' OU 3.5'', selon disponibilite'.
     _
    |_| Documentation plus disquette pour le PC.
        Disquette format 5.25'' impe'rativement.
     _
    |_| Documentation plus disquette pour le PC.
        Disquette format 3.5'' impe'rativement.

    Le montant d'une quelconque de ces commandes est de 120F,
    frais de port inclus, TVA 18,6% incluse. Hors-taxes uniquement pour
    l'e'tranger.

    Re`glement par che`que joint en Francs Franc,ais a` l'ordre de:
    M. l'Agent Comptable de l'INRIA --- CCP 9099-45B Paris

    Nom et pre'nom:
    Adresse:

    Date et Signature


 Rapport Caml:
 -------------
  Pour terminer, j'aimerai beaucoup recevoir votre rapport concernant Caml
 qui me semble tre`s inte'ressant.

 A bientot sur la tribune ...
]