Sunday, 10 February 2008

The power of doing nothing....

There's an ongoing discussion on COCAN on how to make errors explicit in function signatures (the proposed solution is to go exceptionless). I will not delve on why I do not think this is a standard that should be adopted. Instead we will explore a very lightweight solutions that preserves the stack unwinding capability of exceptions whilst making the possible errors explicit in the signatures of the function.

Basic types

When one of our function is applied there we can have either one of two possible outcomes: everything goes right or we are left over with an error (notice the cheap mnemonics). Now if we get rid of exceptions we want our return types to be able all this information. To do so we mimics Haskell's either type:

type ('a,'b) either = Left of 'a | Right of 'b

In case you haden't caught my subtle hints Right is used to hold results and Left to hold errors.

For our short example we shall have a limited number of possible errors:

type possible_exc = [`Too_Small|`Too_Big|`Div_by_zero|`Some_other_error]

that can be thrown in an exception:

exception MyExc of [< possible_exc]

(Allthough I may not be using any unsafe features of OCaml I am actually exploiting a bug in the type-checker here. The absence of this hack would make one of our functions a little less precise).

External interface

Ideally we'd want to choose functions should raise an exception or return a wrapped value. This choice has to be made at function application. Bearing this in mind our external interface is:

module type External = sig
  type ('a,'b) value constraint 'a = [< possible_exc ]
  val run : ('a -> ('b,'c) value) -> 'a -> 'c
  val run_exn : ('a -> ('b,'c) value) -> 'a -> ('b,'c) either
end

Internal interface

The idea behind this implementation is to use a phantom type attached to a value we shall pass along. This phantom type will be unified with every single single value we might raise thus acting as a "collector" for all the possible exceptions. Without further ado let proceed:

module type Internal = sig
  type 'a t constraint 'a = [< possible_exc ]
  type ('a,'b) value constraint 'a = [< possible_exc ]
  val create : unit -> 'a t
  val raise : 'a t -> 'a -> 'b
  val return : 'a t -> 'b -> ('a,'b) value
  val lift : 'a t -> ('a,'b) value -> 'b
end

The type t is our collector. It can only be created via the create function. raise and return are rather self explanatory, lift might come as more of a surprise: it is used to get the returned values from one our function. It ensures the possible errors of the called functions are unified with the "collector" of the callee. The internal interface does not expose functions like External.run because it discards the possible error cases.

Implementation

Our interfaces being set we will now present an implementation. It has been stated at the beginning of this post that we want it as lightweight as possible. Since we will (ab)use the identity functions let's get it out of the way:

let ident = fun i -> i

We are not using the more efficient external "%identity" function because it is, in essence, not type safe. If we consider that the unit value is a value that carries no information (the unit type being inhabited by only one value) and the identity function is a function that does nothing our implementation really doesn't do much:

module Impl = struct
  type 'a t = unit constraint 'a = [< possible_exc ]
  type ('a,'b) value = 'b constraint 'a = [< possible_exc ]
  let create = ident
  let raise () e = raise (MyExc e)
  let return () = ident
  let run = ident
  let lift () = ident
  let run_exn f v = try Right (f v) with  MyExc v -> Left v
end

Excercising it

Let's take our shiny new modules for a test run. The types commented are the inferred types and thus the most general ones.

module I:Internal = Impl

(* int -> ([< possible_exc > `Too_Big `Too_Small ], unit) I.value *)
let check_range i =
  let t = I.create () in
  if i > 5 then
    I.raise t `Too_Big
  else if i < -5 then
    I.raise t `Too_Small
  else
    I.return t ()

(* 'a -> int -> ([< possible_exc > `Div_by_zero ], int) I.value *)
let div x y =
  let t = I.create () in
  if y = 0 then
    I.raise t `Div_by_zero
  else
    I.return t 0

(*
 int ->
 int ->
 ([< possible_exc > `Div_by_zero `Too_Big `Too_Small ], int) I.value
*)
let div_in_range x y =
  let e = I.create () in
  I.lift e (check_range x);
  I.lift e (check_range y);
  I.return e (I.lift e (div x y))

Conclusion

Even though this actually works it does not scale well to multiple modules. It should be considered as a proof of concept rather than serious code.

As there name imply exception should be used to handle exceptional cases. A well designed library should only throw exception when it encounters an error or a bug. Exception should only be used for error recovery (they might be used internally for hacks such as bugtracking but should never trickle out of the library). It seems cumbersome to impose the callee of library functions to handle a long trail of more and more exotic error cases.

If one really desires to have explicit error handling combining our either type with monads seems to be the sane route. This is exactly what the haskell error monad does.

Talking about haskell, an interesting read is 8 ways to report errors in Haskell. It gives a good overview on how messy and uncoherent error reporting can get.

10 comments:

Yoric said...

Mmmmh.....

Looks quite similar to my own implementations. I guess I beat you by about 3 weeks then :)

Till said...

I hadn't looked at your source code before.
I was assuming, given the interface and the fact you were using monads that you were not doing something around these lines.
Now that I have looked at your source code I have a few comments:
_Monads introduce unnecessary lambda expressions. This is due to the fact that exceptions are really an effect function application, you should consider using arrows to encapsulate your data. Converting large chunks of code to monadic style or arrow style is also cumbersome on the programmer. To be fair your code should include examples where the flow is less trivial.
_The universal type introduces boxing. Use Obj.t (which is converted via an %identity) or an abstract type (which you convert also via an %identity like Obj.magic)
_ I do not investigate your code any further but I'm pretty sure it can be used to circumvent type safety... not pretty. (can try to look into it if you want me to).

As before I remain very skeptical towards any attempt to render obsolete OCaml's native handling....

yoric said...

Let me be clear: I never believe that there was any plagiarism, just that we had had similar ideas almost simultaneously.

Now, regarding your remarks,

* Indeed, monads do introduce unnecessary lambdas. We have another Obj.magic-based implementation with a total of only one lambda. I didn't introduce that version as it didn't have the exact same interface as the two other implementations.

* Indeed, we could optimize away some boxing.

* I'm pretty sure that the implementation using references is type-safe. I'm not 100% sure about the implementation I've given which uses Obj.magic, but I'm pretty sure that the faster Obj.magic-based version is type-safe. I'll try and publish that one.

Now, the idea is not to render obsolete OCaml's native handling. Just to add a higher-level library on top of it.

Till said...

Rereading my comment I think I came across as a little too brash, I must have been having a bad day.
I had a closer look at your implementation and the obj.magic actually seems pretty well boxed away. This serves me right for doing crazy assumptions. I still need to wrap my head properly around it, but it seems correct. Obj.magic can be scary because it can mislead the compiler in doing some unsafe optimisations.

Arrows are more confidential than monads and harder to grasp (the arrow notation just doesn't cut it...). So I think ideally we would provide both.

As a side note I never felt accused of plagiarism. And, although I maintain part of my skepticism I consider explicit error to be a good thing in some situations (we use it here in some critical code, when you are dealing with sensible systems it is nice to know they won't crash and burn on the first glitch encountered).

yoric said...

[Just for the information, Till, Arnaud and I are currently working together on a new version of this idea. We manage to achieve quite acceptable performances and minimal intrusivity. Stay tuned for more info...]

Till said...

Let me rectify this:
I keep on babling incoherent stuff while in the meantime David is happily hacking away 1000's of lines of code...

Gaël said...

Tiens, t'as un blog, toi. :->. J'étais en croisière avec François Garillot la semaine dernière en Grèce et je lui ai piqué le cours d'introduction à la logique de Girard. Cela me rappelle une croisière en Grèce il y a quelque temps, ... J'ai eut le temps d'arriver jusqu'au système F, mais je dois dire que j'ai lu cela avec une attention moyenne.

Anonymous said...

After getting more than 10000 visitors/day to my website I thought your till-varoquaux.blogspot.com website also need unstoppable flow of traffic...

Use this BRAND NEW software and get all the traffic for your website you will ever need ...

= = > > http://get-massive-autopilot-traffic.com

In testing phase it generated 867,981 visitors and $540,340.

Then another $86,299.13 in 90 days to be exact. That's $958.88 a
day!!

And all it took was 10 minutes to set up and run.

But how does it work??

You just configure the system, click the mouse button a few
times, activate the software, copy and paste a few links and
you're done!!

Click the link BELOW as you're about to witness a software that
could be a MAJOR turning point to your success.

= = > > http://get-massive-autopilot-traffic.com

Anonymous said...

[url=http://www.casino-online.gd]casinos online[/url], also known as eminent casinos or Internet casinos, are online versions of urgent ("buddy and mortar") casinos. Online casinos distribute gamblers to get domain a adverse in and wager on casino games tailback the Internet.
Online casinos usually make an indecent up championing nearby odds and payback percentages that are comparable to land-based casinos. Some online casinos contend higher payback percentages as a peacefulness into deficiency extend games, and some bruit about payout participation audits on their websites. Assuming that the online casino is using an correctly programmed unsystematic thicket generator, recount games like blackjack want an established congress edge. The payout shard preferably of these games are established erstwhile the rules of the game.
Heterogeneous online casinos commission in default or tussle their software from companies like Microgaming, Realtime Gaming, Playtech, Pestilence Imposture Technology and CryptoLogic Inc.

Anonymous said...

http://hapna.com/pre/buypropeciaonline/#10846 generic propecia erfahrung - buy propecia proscar