[Caml-list] "polymorphic" exceptions?

[Caml-list] "polymorphic" exceptions?

[Markus Mottl]

Hello,

not long ago there was an article here about using type variables to
parameterize local modules. I just came across a class of problems
where this seems like a very nice feature: having "polymorphic"
exceptions. E.g.:

  type index

  let add ord_el (el : 'el) map =
    let module M =
      struct
        exception Found of index * 'el
      end in
    try
      (* try to add new node or raise exception if key already exists *)
      ...
    with Found (index, node) ->
      update_node index { node with el = el } map.nodes

It is really a pity that it is not allowed to write

  exception Found of index * 'el

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.

As was mentioned in the former article, one can also use this trick to
parameterize local functor arguments using type variables that are bound
in the enclosing expression: surely also useful more often than once.

Is there any chance that this could be added to the language? This
wouldn't introduce any new concepts, but make some cases more general.

Best regards,
Markus Mottl

-- 
Markus Mottl, mottl@miss.wu-wien.ac.at, http://miss.wu-wien.ac.at/~mottl
-------------------
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

Re: [Caml-list] "polymorphic" exceptions?

[CREGUT Pierre FTRD/DTL/LAN]

Ok, i didn't reply to your first post immediately, so here is my 5 cents 
answer .

Pierre

Quoting Markus Mottl (mottl@miss.wu-wien.ac.at):
> 
> 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.

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.

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

-- 
Pierre Cregut - pierre.cregut@rd.francetelecom.com - +33 2 96 05 16 28
FTR&D - DTL/MSV - 2 avenue Pierre Marzin - 22307 Lannion Cedex - France
-------------------
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

Re: [Caml-list] "polymorphic" exceptions?

[Markus Mottl]

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