Version française
Home     About     Download     Resources     Contact us    
Browse thread
[Caml-list] "polymorphic" exceptions?
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: Markus Mottl <markus@m...>
Subject: Re: [Caml-list] "polymorphic" exceptions?
On Thu, 19 Jul 2001, CREGUT Pierre FTRD/DTL/LAN wrote:
> > even though the type variable is bound in "el : 'el". This seems perfectly
> > safe to me, because only the body of "add" can see the module and knows
> > what 'el is when catching the exception. Code outside cannot access the
> > module and therefore cannot catch the exception, which could be unsound if
> > 'el is not known at this point.

> I don't understand what you mean by "cannot access". add can give
> back functions and you can also register functions with callbacks via
> global references directly in the code of the module even if they were
> restricted to the unit -> unit type or (unit -> unit) -> unit.

The type of the reference couldn't be generalized if it involved 'el. If
it doesn't, there is nothing wrong with it. The type checker wouldn't
allow you to do anything unsound within closures, no matter whether the
closure can be called in a context where the local module is visible
or not: type correctness is verified in the place where the closure is
created and the module is necessarily visible there, which provides all
information to the typechecker that it needs to know.

> Those functions can raise exceptions or catch them (eg. functional
> catching the exceptions raised by their function argument and printing
> it back or whatever).
> So your exception CAN escape the scope of add and you can mix an
> exception created by one call to add with one given type, with a catcher 
> created by another call with another type.

Note what Pierre just recently said:

  Exception definitions are generative in Caml: it means that the
  definition of two exceptions with the same names generate two different
  exceptions that are not confused by the language. It is similar to
  type definitions, and constructors for sum type.

This means that even calling the polymorphic function twice with the
_same_ type of value would still generate local exceptions that are
incompatible, i.e. a closure returned by the first call to "add" cannot
throw a local exception that can be caught by a closure that is returned
by a second call to "add" - even if this were sound!

> exception tags are defined at link time as far as I know.
> They are not so dynamic so that you can compile matching.

I don't think that this has anything to do with type variables used
in local exception definitions. Even now (without polymorphism) the
exception cannot be caught by a different closure, e.g.:

  let foo () =
    let module M = struct exception E end in
    let throw () = raise M.E in
    let catch f = try f () with M.E -> assert false in
    throw, catch

  let _ =
    let throw1, catch1 = foo () in
    let throw2, catch2 = foo () in
    catch2 throw1

This won't catch the exception, whereas "catch2 throw2" will, of course,
which leads to an assertion failure instead. I don't see any reason why
this shouldn't work the same way with type variables in the exception
definition. Or am I misunderstanding your argument?

Regards,
Markus Mottl

-- 
Markus Mottl                                             markus@oefai.at
Austrian Research Institute
for Artificial Intelligence                  http://www.oefai.at/~markus
-------------------
Bug reports: http://caml.inria.fr/bin/caml-bugs  FAQ: http://caml.inria.fr/FAQ/
To unsubscribe, mail caml-list-request@inria.fr  Archives: http://caml.inria.fr