This site is updated infrequently. For up-to-date information, please visit the new OCaml website at ocaml.org.

environment idiom
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
 Date: 2004-12-13 (05:41) From: skaller Subject: Re: [Caml-list] environment idiom
```On Mon, 2004-12-13 at 13:03, Michael Walter wrote:

> It is probably better to say "from the outside it is pure, and inside
> it appears impure, relative to its boundary" (thus stressing the point
> that your apparent impurity is only a "view" <wink>).

Perhaps so.

> I think the problem is that we are using "pure" twofold here:

Yes. But this is not all ..

> a) As an (absolute) property of the language
> b) As the property of code (which is relative to its environment)
>
> As you can obviously emulate impurity in a pure language (see State
> monad), and code pure in a impure language, it is not much of a
> surprise that b) can differ from a).

Consider this example. We have an algorithm, such as:

Take an array of bool length n initially all false.
for i = 1 to n do
if element i is false
print i
set every i'th element true

Of course this is the Sieve. Now consider a
procedural and functional implementation.

We can ask: is the implementation *correct*?
In this case, probably it is easier to reason about
the correctness of the procedural implementation than
the functional one (although I wouldn't bet on it :)

We can also ask: is the algorithm correct? (At finding primes).

That's a different question about a different level of the
encoding.

Finally we can ask: are the functional and procedural
programs correct (at finding primes)?

I am desiring to show here that 'the ability to
reason about correctness' depends on what encoding

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.

So we're agreeing on the ideas, but we need some
way to *distinguish* in a less informal way,
that a Haskell program may not be as 'pure' at all
levels as the detailed encoding is.

Whilst this isn't restricted to Haskell, given
to see what higher level abstractions they represent,
and how pure they are, in the abstract, and thus
make -- or find it harder to make -- judgements,
depending on how 'transparent' that abstraction is.

because not only do monads localise the code that
needs this special consideration, but the typeclasses
systematically present the structure, so you can
extend your normal inference rules to cover the

It would seem than that for some monads, the extension
inference rules would be harder to use since they don't
include rules that require transparency. The advantage
is that you can still reason about the code, and you can
even say which inference rules can be applied where.

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.

--
John Skaller, mailto:skaller@users.sf.net
voice: 061-2-9660-0850,
snail: PO BOX 401 Glebe NSW 2037 Australia
Checkout the Felix programming language http://felix.sf.net

```