From mboxrd@z Thu Jan  1 00:00:00 1970
Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id PAA31677 for caml-red; Sun, 19 Nov 2000 15:56:30 +0100 (MET)
Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id SAA03011 for <caml-list@pauillac.inria.fr>; Fri, 17 Nov 2000 18:17:59 +0100 (MET)
Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35])
	by concorde.inria.fr (8.11.1/8.10.0) with ESMTP id eAHHHjj23710;
	Fri, 17 Nov 2000 18:17:45 +0100 (MET)
Received: (from xleroy@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id SAA31562; Fri, 17 Nov 2000 18:17:44 +0100 (MET)
Message-ID: <20001117181744.49309@pauillac.inria.fr>
Date: Fri, 17 Nov 2000 18:17:44 +0100
From: Xavier Leroy <Xavier.Leroy@inria.fr>
To: Michel Levy <Michel.Levy@imag.fr>, caml-list@inria.fr
Subject: Re: pourquoi y-a-t-il des exceptions?
References: <3A1419FD.CE44DEA4@imag.fr>
Mime-Version: 1.0
Content-Type: text/plain; charset=iso-8859-1
Content-Transfer-Encoding: 8bit
X-Mailer: Mutt 0.89.1
In-Reply-To: <3A1419FD.CE44DEA4@imag.fr>; from Michel Levy on Thu, Nov 16, 2000 at 06:31:41PM +0100
Sender: weis@pauillac.inria.fr

[English summary: 1- exception declarations are generative, so there
is a "global state" for exceptions already declared; 2- if "raise"
could throw any value as an exception, there would be no way to match
on the exception just caught in the try ... with ... construct.]

> Je me livre (pour le compte de mes étudiants) à une introspection de
> Caml, en essayant d'introduire les exceptions dans le langage
> mini-Caml du livre "Le langage Caml" de Pierre Weiss et Xavier Leroy.
> Pour faire bien les choses, j'ai commencé par lire la définition de
> Standart ML et je n'ai pas compris les règles de liaisons des 
> eceptions (règle 130). Pourquoi dans cette définition un état d'un
> programme doit-il comporter non seulement l'état de la mémoire
> mais aussi les noms des exceptions ?

Je n'ai pas la Definition sous les yeux, mais je crois que c'est pour
respecter le comportement génératif des déclarations d'exceptions.
C'est-à-dire, si le programme évalue deux fois la déclaration
"exception E", deux exceptions différentes de nom "E" sont créées.
(Cela peut se produire avec des foncteurs, ou bien avec "let exception
... in" en SML, ou bien avec "let module ... in" en OCaml.)

Pour rendre compte de cela dans la sémantique formelle, on peut utiliser
une espèce de "store" (état mémoire global) qui garde trace des exceptions
déjà déclarées.  Je pense que c'est ce que qui est fait dans The
Definition of SML.

> Et d'ailleurs pourquoi y-a-t-il le type exception, ne pourrait-on pas
> appliquer "raise" à n'importe quelle valeur qui deviendrait une
> exception déclanchée (cf règle 107 de la définition de Standart ML) ?

Cela ne poserait pas de problème au niveau du "raise", mais cela
poserait problème pour typer le "try...with..."  ("handle" en SML).
En effet, la valeur de l'exception rattrapée serait alors d'un type
quelconque, inconnu statiquement, ce qui empêcherait d'en faire quoi
que ce soit dans la partie "with" du "try...with...", en particulier
de la filtrer.

- Xavier Leroy