From mboxrd@z Thu Jan 1 00:00:00 1970 Received: by margaux.inria.fr, Tue, 6 Oct 92 20:13:54 +0100 Received: from concorde.inria.fr by margaux.inria.fr, Tue, 6 Oct 92 17:44:08 +0100 Received: from chx400.switch.ch by concorde.inria.fr; Tue, 6 Oct 92 17:46:31 +0100 X400-Received: by mta chx400.switch.ch in /PRMD=switch/ADMD=arcom/C=CH/; Relayed; Tue, 6 Oct 1992 13:36:41 +0100 X400-Received: by /PRMD=SWITCH/ADMD=ARCOM/C=CH/; Relayed; Tue, 6 Oct 1992 13:38:52 +0100 Date: Tue, 6 Oct 1992 13:38:52 +0100 X400-Originator: diderich@lithsun1.epfl.ch X400-Recipients: caml-light@margaux.inria.fr X400-Mts-Identifier: [/PRMD=SWITCH/ADMD=ARCOM/C=CH/;9210061238.AA02414] X400-Content-Type: P2-1984 (2) From: "(Claude Diderich)" Message-Id: <9210061238.AA02414@lithsun1.epfl.ch> To: caml-light@margaux Cc: diderich@di.epfl.ch Subject: Possible bug report in CAML Light V0.5 Received: from lithsun1.epfl.ch by SIC.Epfl.CH via INTERNET ; Tue, 6 Oct 92 13:34:27 N Sender: weis@margaux 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))))));; : (('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 = # 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 ... ]