Possible bug report in CAML Light V0.5

Xavier Leroy (diderich@lithsun1.epfl.ch)
Tue, 6 Oct 1992 13:38:52 +0100

Date: Tue, 6 Oct 1992 13:38:52 +0100
From: "(Claude Diderich)" <diderich@lithsun1.epfl.ch>
Message-Id: <9210061238.AA02414@lithsun1.epfl.ch>
To: caml-light@margaux
Subject: Possible bug report in CAML Light V0.5

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 ...
]