caml-list - the Caml user's mailing list
 help / color / mirror / Atom feed
* pourquoi y-a-t-il des exceptions?
@ 2000-11-16 17:31 Michel Levy
  2000-11-17 17:17 ` Xavier Leroy
  0 siblings, 1 reply; 3+ messages in thread
From: Michel Levy @ 2000-11-16 17:31 UTC (permalink / raw)
  To: caml-list

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 ?
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) ?

I'am trying to write an "Caml introspection", by introducing the
exception in the mini-Caml language 
of Pierre Weiss and Xavier Leroy book "Le langage Caml".
To do that, I have read the definition of Standard ML (revised 1997) and
I don't understand the Exception Binding rules (130).
Why does a program's state include not only the memory state, but also
the exceptions names ?


-- 
Michel Levy  
D106 - L.S.R.     B.P.72 - 38042 SAINT MARTIN D'HERES CEDEX - France
e.mail : Michel.Levy@imag.fr    tel :(33)476827246
http://www-lsr.imag.fr/Les.Personnes/Michel.Levy



^ permalink raw reply	[flat|nested] 3+ messages in thread

* Re: pourquoi y-a-t-il des exceptions?
  2000-11-16 17:31 pourquoi y-a-t-il des exceptions? Michel Levy
@ 2000-11-17 17:17 ` Xavier Leroy
  2000-11-20  8:06   ` Francois Pottier
  0 siblings, 1 reply; 3+ messages in thread
From: Xavier Leroy @ 2000-11-17 17:17 UTC (permalink / raw)
  To: Michel Levy, caml-list

[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



^ permalink raw reply	[flat|nested] 3+ messages in thread

* Re: pourquoi y-a-t-il des exceptions?
  2000-11-17 17:17 ` Xavier Leroy
@ 2000-11-20  8:06   ` Francois Pottier
  0 siblings, 0 replies; 3+ messages in thread
From: Francois Pottier @ 2000-11-20  8:06 UTC (permalink / raw)
  To: caml-list


On Fri, Nov 17, 2000 at 06:17:44PM +0100, Xavier Leroy wrote:
>
> 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.

À moins d'annoter chaque fonction par le type des exceptions
qu'elle est susceptible de renvoyer, de façon similaire à ce
qui est fait dans la thèse de François Pessaux. Cela donne un
système de types beaucoup plus fin et beaucoup plus lourd (au
moins en termes de lisibilité).

Cela dit, d'un point de vue purement opérationnel, on pourrait
très bien considérer que `raise' est applicable à une valeur
quelconque. Le seul langage répandu à avoir adopté ce point de
vue est (à ma connaissance) C++...

--
François Pottier
Francois.Pottier@inria.fr
http://pauillac.inria.fr/~fpottier/



^ permalink raw reply	[flat|nested] 3+ messages in thread

end of thread, other threads:[~2000-11-20 19:22 UTC | newest]

Thread overview: 3+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2000-11-16 17:31 pourquoi y-a-t-il des exceptions? Michel Levy
2000-11-17 17:17 ` Xavier Leroy
2000-11-20  8:06   ` Francois Pottier

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).