From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from majordomo@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id NAA22638; Thu, 19 Jul 2001 13:37:48 +0200 (MET DST) X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f 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 NAA22634 for ; Thu, 19 Jul 2001 13:37:47 +0200 (MET DST) Received: from chopin.ai.univie.ac.at (chopin.ai.univie.ac.at [131.130.174.170]) by concorde.inria.fr (8.11.1/8.10.0) with ESMTP id f6JBbk913903 for ; Thu, 19 Jul 2001 13:37:46 +0200 (MET DST) Received: (from markus@localhost) by chopin.ai.univie.ac.at (8.9.3/8.9.3/Debian 8.9.3-21) id NAA19125; Thu, 19 Jul 2001 13:37:38 +0200 Date: Thu, 19 Jul 2001 13:37:37 +0200 From: Markus Mottl To: CREGUT Pierre FTRD/DTL/LAN Cc: OCAML Subject: Re: [Caml-list] "polymorphic" exceptions? Message-ID: <20010719133737.A18220@chopin.ai.univie.ac.at> References: <20010625152919.A18486@miss.wu-wien.ac.at> <20010719085101.A17284@lat4149.rd.francetelecom.fr> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline User-Agent: Mutt/1.2.5i In-Reply-To: <20010719085101.A17284@lat4149.rd.francetelecom.fr>; from pierre.cregut@rd.francetelecom.com on Thu, Jul 19, 2001 at 08:51:01 +0200 Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk 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