Re: [Caml-list] environment idiom

[Michael Walter <michael.walter@gmail.com>]

On 13 Dec 2004 16:41:23 +1100, skaller <skaller@users.sourceforge.net> wrote:
> [...]
> I am desiring to show here that 'the ability to
> reason about correctness' depends on what encoding
> of what you're asking the question about.
Agreed.

> Clearly even a functional encoding of the Sieve
> is still a procedural program at the level of
> calculating primes. However it is pure at the
> detail level. This only helps, and only perhaps
> helps, at reasoning if the code faithfully implements
> the algorithm -- if you try to reason about it's
> ability to calculate primes you inevitably have to
> account for the fact the algorithm isn't functional.
What is "the detail level"? Like the "language level" in contrast to
the level of the current abstraction (for instance, State monad)?

Different note: I think you are missing out an important property of
the functional encoding, which is its purity wrt composability.
Suppose one of the few obvious types of the sieve, for instance:
  sieve :: Integer -> [Integer]
You can clearly see that the sieve is a pure function, and actually
the type system proves this for you (modulo cheating, err,
unsafePerformIO et al). This makes it very easy and safe to use the
function (and also to test it, btw!).

In constrast, in a language such as C++ you cannot assume that..
  vector<unsigned> sieve(unsigned);
has no side effects.

Also consider the "print" part of your algorithm, which I ignored so
far. In C++ it would be very easy to add it to sieve() thus making the
function virtually useless to use but in the special case where you
want to print the number instantly.

In Haskell, you *could* have a sieve :: Integer -> IO [Integer], but
what you would really do is to decouple the sieve and I/O (and this is
made kinda "attractive" by the expressiveness of the language and the
type system). So what you would do is something like:
  printPrimes :: Integer -> IO ()
  printPrimes :: mapM_ print . sieve
(modulo obvious types made at 4 AM :-)

There is also an interesting point about algorithms which I'm sure you
are aware of. Often when analyzing algorithms for their correctness,
you reason about the state before and after a certain step in the
algorithm. That is, you make the state and its change explicit. Sounds
like sieveStep :: State -> State, huh? :-) I think that is also what
makes monads in Haskell attractive. They are very nice to use from a
programmer's perspective (IMO), but they also allow good reasoning (as
they are usually purely defined or at least definable).

> This is probably harder to do in Ocaml, where the
> places that transparency is lost aren't so easy to
> find, and the effects on the whole program not quite
> so easy to isolate.
Yep! Monads actually allow nice embedding of many paradigms, not only
the imperative.

4:29 AM-ly yours,
Michael