The Axis of Eval (was: More cores)

[Dario Teixeira <darioteixeira@yahoo.com>]

Hi,

> Erlang makes concurrency easy due to purity, and OCaml is
> famous for being eclectic.  Why not embrace Erlang's
> model by imposing limitations on what can be in threads --
> keeping them pure?

Indeed.  Ocaml's imperative features can be very useful in a local context
(ie, not crossing the boundaries of a function), but do hinder concurrency
when used for modifying global state.  I wonder: is there already a tool
that verifies Ocaml code to ensure that a function is pure?  Something
along the lines of Ocamlexc, but applied to purity.

The way I see it, there are (at least) three axis associated with a
function: the value axis, the exception axis, and the purity axis (the
latter can also be called the side-effect axis). In Ocaml, a function
signature cares only about the value axis, though implicitly the other
axis are also be present.  For example:

val integer_division: int -> int -> int
    throws Division_by_zero
    is_pure

val incr_global_counter: unit -> unit
    throws_nothing
    is_not_pure

I can imagine a "spawn" statement in a concurrent Caml that expects
that the function passed as parameter be pure.  And of course a function
would only be pure if it did not modify global state and only invoked
pure functions itself.

Obviously the other alternative is to go the Haskell route and transform
Caml in a pure functional language where monads reign.  Though I think it
would be interesting to come up with a solution that keeps the advantages
of local imperative features, but does ensure purity for the purpose of
concurrency.

(and I'm sure there is already a ton of research along these lines)

Cheers,
Dario Teixeira