[Caml-list] Checked exceptions and type inference

[Caml-list] Checked exceptions and type inference

[Brian Hurt]

Reading LtU I came across this article:
http://www.octopull.demon.co.uk/java/ExceptionalJava.html

Java treats checked exceptions as part of the type signature of the 
function.  As such, it seems to me that as such, type inference would work 
to propogate most of this information in a more convient way.

Checked exceptions actually have their uses, for "errors" which are not 
very exceptional.  Out of memory is highly unexpected.  End of file isn't 
quite as surprising.  Not_found is another that shouldn't be that 
surprising- although that leads to a different religous war.

Is there any research on using checked exceptions in an ML derived 
language?  Any plans/opinions on implementing checked exceptions in Ocaml?

Brian


-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Checked exceptions and type inference

[Jacques Garrigue]

From: Brian Hurt <brian.hurt@qlogic.com>

> Java treats checked exceptions as part of the type signature of the 
> function.  As such, it seems to me that as such, type inference would work 
> to propogate most of this information in a more convient way.
[...]
> Is there any research on using checked exceptions in an ML derived 
> language?  Any plans/opinions on implementing checked exceptions in Ocaml?

I'm not sure it is exactly what you are looking for, but Francois
Pessaux wrote a PhD thesis (and also implemented it) on "static
analysis to detect uncaught exceptions in Objective Caml". IIRC, you
need to declare nothing, the checker tells you what exceptions can
happen at any point of the program.

http://guinness.cs.stevens-tech.edu/~fpessaux/#My_thesis_work

I suppose the same technology could also be used in a more defensive
manner: checking that only specified exceptions can come out of a
function for instance.

Jacques Garrigue

-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Checked exceptions and type inference

[Xavier Leroy]

> Is there any research on using checked exceptions in an ML derived 
> language?  Any plans/opinions on implementing checked exceptions in Ocaml?

As Jacques mentioned, you can look at François Pessaux's work, e.g.
our TOPLAS article
   http://pauillac.inria.fr/~xleroy/publi/exceptions-toplas.ps.gz

Briefly, Java-style exception declarations just don't work with
higher-order functions and parametric polymorphism.  For ML, you need
row polymorphism on the exception declarations to achieve sufficient
precision, and the resulting types are complicated enough that you
don't want to write them in module interfaces.  The solution François
explored is to infer completely these exception annotations with a
whole-program analysis.

- Xavier Leroy

-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Checked exceptions and type inference

[Stefano Zacchiroli]

On Wed, Mar 12, 2003 at 09:45:05AM +0100, Xavier Leroy wrote:
> http://pauillac.inria.fr/~xleroy/publi/exceptions-toplas.ps.gz

Is this work supposed to be included in future ocaml releases?

Thanks,
Cheers.

-- 
Stefano Zacchiroli  -  Undergraduate Student of CS @ Uni. Bologna, Italy
zack@{cs.unibo.it,debian.org,bononia.it}  -  http://www.bononia.it/zack/
"  I know you believe you understood what you think I said, but I am not
sure you realize that what you heard is not what I meant!  " -- G.Romney

-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Checked exceptions and type inference

[Xavier Leroy]

> On Wed, Mar 12, 2003 at 09:45:05AM +0100, Xavier Leroy wrote:
> > http://pauillac.inria.fr/~xleroy/publi/exceptions-toplas.ps.gz
> 
> Is this work supposed to be included in future ocaml releases?

François Pessaux's exception analyzer is distributed separately:
        http://caml.inria.fr/ocamlexc/ocamlexc.htm
However, by lack of a maintainer, it wasn't updated to cover the
latest OCaml features; I believe the analyzer is based on OCaml 2.04
or perhaps 3.00.

- Xavier Leroy

-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Checked exceptions and type inference

[Richard W.M. Jones]

On Tue, Mar 11, 2003 at 03:50:13PM -0600, Brian Hurt wrote:
> Is there any research on using checked exceptions in an ML derived 
> language?  Any plans/opinions on implementing checked exceptions in Ocaml?

Please no.

Having written the following thousands of times I am no fan of
checked exceptions ...

try {
  ... the code I WANTED to write ...
}
catch (IOException ex) {
  throw new UncheckedWrapperException (ex);
}
catch (SecurityException ex) {
  throw new UncheckedWrapperException (ex);
}
catch (SomeException ex) {
  throw new UncheckedWrapperException (ex);
}
catch (AnotherException ex) {
  throw new UncheckedWrapperException (ex);
}
catch (SomeOtherException ex) {
  throw new UncheckedWrapperException (ex);
}

Rich.

-- 
Richard Jones, Red Hat Inc. (London, UK) http://www.redhat.com/software/ccm
http://www.annexia.org/ Freshmeat projects: http://freshmeat.net/users/rwmj
PTHRLIB is a library for writing small, efficient and fast servers in C.
HTTP, CGI, DBI, lightweight threads: http://www.annexia.org/freeware/pthrlib/

-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

[Caml-list] Checked exceptions and type inference

[William Chesters]

Brian Hurt writes:
 > Is there any research on using checked exceptions in an ML derived 
 > language?  Any plans/opinions on implementing checked exceptions in Ocaml?

Java checked exceptions are a huge pain because the checking is too
monomorphic.  Here's a trivial example:

  int numElements(Enumeration e) {
    for (int i = 0; e.hasMoreElements(); ++i) e.nextElement();
  }

  System.out.println(numElements(new LinesInFileEnumeration("foo.txt"));

This fails because LinesInFileEnumeration wants to throw IOException,
while the Enumeration interface won't let it.  To work around this you
have to

  -- explicitly catch and re-wrap exceptions into some form acceptible
     for the interface you want to implement, at more or less every
     package boundary (not only boring but also functionally bad---
     what am I supposed to do with a wrapped exception? how can I
     tell at a higher level that it is really an IOException? and
     it really interacts badly with the debugger ...)
     
  or make practically every method in your program able to throw
     practically any exception.  Much real Java code ends up this way,
     with methods throwing apparently irrelevant IOExceptions and
     SQLExceptions left right and centre.  The infection spreads
     very quickly.

  or make all your exceptions RuntimeExceptions.  This is actually
     the best solution---bypass the "checked exception" system entirely.

Maybe a more polymorphic kind of exception "type checking" would be
less annoying, but I also don't think it would really achieve
anything.

-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Checked exceptions and type inference

[Brian Hurt]

On Wed, 12 Mar 2003, Richard W.M. Jones wrote:

> On Tue, Mar 11, 2003 at 03:50:13PM -0600, Brian Hurt wrote:
> > Is there any research on using checked exceptions in an ML derived 
> > language?  Any plans/opinions on implementing checked exceptions in Ocaml?
> 
> Please no.

I'm not sure where I sit in this debate.

On one hand, if you view exceptions as 'error returns' (End of File, etc),
then checked exceptions make sense.  Some errors need to be handled.  And
handling them should be required.  On the other hand, if you view
exceptions as 'probably fatal exceptional conditions' (Out of Memory, 
etc), then having to deal with them is simply a nuisance.  What else can 
you do except print out an error message, clean up, and exit?

Now, for the trick question: is Not_found an error return, or a probably 
fatal exceptional condition?

And yes, I've had fun with Java exceptions as well, which is the only 
reason I'm wimbling.  And failure modes do expose the internal workings of 
an object (or a function, or whatever atom of generalization you are 
using).

Brian


-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

RE: [Caml-list] Checked exceptions and type inference

[mgushee]

On 11 Mar 2003 at 22:00, Arturo Borquez wrote:

> Brian Hurt <brian.hurt@qlogic.com> wrote:

> >Java treats checked exceptions as part of the type signature of the
> >function.  As such, it seems to me that as such, type inference would work
> >to propogate most of this information in a more convient way.

>  let x = try String.sub str pos len with _ -> "" in
>  ....
> 
> in this case failing String.sub is returning a string,
> and the type inference system will check it that way.
> 
> Perhaps I don't understand what migth be a
> 'checked exception' in ML. I am missing something?.
> can you explain it with an example?

I guess you must be unfamiliar with Java terminology. A checked 
exception is one that the programmer must provide for in any method 
that can raise it, either by writing a handler or by indicating in 
the method signature that the method may raise that exception. 
They're called "checked" because the compiler checks whether they are 
handled. For example, if you have a method getConfig() that reads a 
configuration file, you have to provide for possible I/O errors: 
either

    try {
        /* open and read file */
    } catch (IOException e) {
        /* handle exception */
    }

Within the body of the method, or a signature such as:

    public HashTable getConfig() throws IOException {
        /* do whatever */
    }

so in the latter case, the exception is indeed part of the method 
signature.

Unchecked exceptions are generally those resulting from unpredictable 
conditions, such as OutOfMemoryError, NullPointerException, and 
ThreadDeath.

--
Matt Gushee
Englewood, CO USA

-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Checked exceptions and type inference

[Nicolas Cannasse]

> Perhaps I don't understand what migth be a
> 'checked exception' in ML. I am missing something?.
> can you explain it with an example

Checked exception are like in Java : the compiler warn you if you don't
catch them, and if you really don't want to do so, you have to put an
annotation on your fonction to say that it is throwing this kind of
exception.
For example

File openFile( String filename ) {
    return new File(filename);
}

compiler warn you about the IOException that can be thrown by the call to
"new File" and so you have either to ignore it :

File openFile( String filename ) {
    try {
        return new File(filename);
    } catch( IOException e ) {
        // print it if you feel like
        return null;
    }
}

or to propagate it explicitly

File openFile( String filename) throws IOException {
    return new File(filename);
}

but then the calling function of openFile will have also to decide either to
catch or to throw the IOException.
That's quite a rigorous way of handling exceptions, and you can use the
RuntimeException class to use exceptions à la OCaml.

BTW, I really dislike checked Exceptions, but I realy you want to support
them, here's some tip :

type 'a checked =
    | Result of 'a
    | Exc of exn

let check f x =
    try
        Result ( f x )
    with
        e -> Exc e

and then you can use it like this when you catch the exception :

let open_file filename =
    match check open_out filename with
    | Result x -> x
    | Exc e -> (* do something *)

or when you want to propagate it :

let open_file filename = check open_out filename

Nicolas Cannasse

-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

RE: [Caml-list] Checked exceptions and type inference

[Arturo Borquez]

Brian Hurt <brian.hurt@qlogic.com> wrote:

>
>Reading LtU I came across this article:
>http://www.octopull.demon.co.uk/java/ExceptionalJava.html
>
>Java treats checked exceptions as part of the type signature of the
>function.  As such, it seems to me that as such, type inference would work
>to propogate most of this information in a more convient way.
>

>From the manual:
Caml provides exceptions for signalling and handling exceptional conditions. ...

These 'exceptional conditions' do not implies an 'error'
at all, so it might be. Moreover exceptions may have a type
within the context where they occurr. ie:

 let x = try String.sub str pos len with _ -> "" in
 ....

in this case failing String.sub is returning a string,
and the type inference system will check it that way.

Perhaps I don't understand what migth be a
'checked exception' in ML. I am missing something?.
can you explain it with an example?

>Checked exceptions actually have their uses, for "errors" which are not
>very exceptional.  Out of memory is highly unexpected.  End of file isn't
>quite as surprising.  Not_found is another that shouldn't be that
>surprising- although that leads to a different religous war.
>
>Is there any research on using checked exceptions in an ML derived
>language?  Any plans/opinions on implementing checked exceptions in Ocaml?
>

Regards.

-- 
Arturo Borquez


__________________________________________________________________
Try AOL and get 1045 hours FREE for 45 days!
http://free.aol.com/tryaolfree/index.adp?375380

Get AOL Instant Messenger 5.1 for FREE! Download Now!
http://aim.aol.com/aimnew/Aim/register.adp?promos=380455

-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners