Re: [Caml-list] environment idiom

[skaller <skaller@users.sourceforge.net>]

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
of what you're asking the question about.

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
monads it seems we can focus on the monadic parts
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.

In other words, I guess Haskell monads are good,
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
monadic code.

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