Re: [Caml-list] environment idiom

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

On 13 Dec 2004 17:18:36 +1100, skaller <skaller@users.sourceforge.net> wrote:
> On Mon, 2004-12-13 at 13:45, Michael Walter wrote:
> > > The claims that monadic programming allows side effect
> > > free transparent purely functional encoding is unquestionably
> > > bogus.
> > In your view, would claiming that the stream approach allowed that be
> > bogus as well?
> [..]
> With that idea in mind, any claim that X is transparent is automatically
> bogus without context, you really need to say instead
> 
>         "X is transparent at the Y level"
Right. But very often (such as in "mine is bigger" <0.5 wink>), the
comparison argument ("the context") is obvious and/or has a typical
meaning: If you say that "monadic programming allows side effect free
transparent purely functional encoding of state", most people will
understand what you are talking about (the State monad allows apparent
stateful computations, but can be purely functionally encoded).

You are stressing a different but no less obvious point of monads, in
this example that a State monad models state (i.e. you have apparent
statefulness *inside* the monad).

> Another example is my Felix language. It has both functions
> and procedures. Functions aren't allowed to have side effects,
> yet they're not pure in the sense the result can depend
> on variables which change between (but not during) invocations.
> [This has an alarming effect on the optimiser ..]
Can I read about the reasoning behind this on felix.sf.net?

> [...] Clearly you can reason about the
> 'functional subsystem' using transparency, and then combine
> the result with reasoning about the top level 'magic main'
> where the program as a whole is not transparent ... and you still
> have 'ease of reasoning' in the combination.
Indeed (and Monads give you an attractive way to partly do this the
other way around).

> Yes, but that is precisely the point. In wishing to avoid
> the kind of hype normally associated with OO and Java,
> I think it is necessary to reconsider exactly what
> crude statements like 'it is pure and transparent' actually
> mean.
Are there specific statements, for instance on the Haskell home page,
which you dislike? Or do you dislike that fact that for instance in
the statement "Monads allow for sideeffect free encoding of stateful
computations" everyone is assuming that "encoding" refers to the
encoding in the target language?

> It was actually *my* statement that I labelled 'unquestionably
> bogus', namely that Haskell (including all monadic programming)
> is pure and transparent (and side effect free) when clearly
> any kind of I/O at the OS level is not.
Okay, I was thinking (along the lines of the paragraph above) that you
were unhappy about the way that people are talking about monads.

> However the claim is not *wrong*, instead I'm claiming
> it isn't a well formed formula: 'pure' is a predicate
> that has to be applied to a particular level of encoding,
> and then you can reason about that level using that
> property.
Okay. So far I have never been confused by such statements about
monads -- it was usually pretty clear what "pure" was referring to (Of
course stateful computations deal with state, that is the very point
of them. But OTOH it is very obvious that calling the State monad
"pure" does not talk about computations *inside* the State monad, but
about the *outside* view -- if you run a computation in the State
monad, the result _purely_ depends on the arguments of runState).

> ... but that isn't enough to reason about correctness,
> since it invariably means checking the program meets some
> specification given at a much higher level of abstraction.
Sure.


> Since I'm not a Haskell programmer it is hard to give examples,
> but for Ocaml I'm sure we all know that some uses of
> imperative programming technique feel 'safer' than others.
> They threaten purity less. But this is just waffle.
> I'd like to have a better guideline.
I'm not an O'Caml programmer but I think I know what you mean.

> Why are localised uses of mutation
> less of a threat to reasoning than less localised ones?
> 
> Because it's encapsulated in the function .. but that is
> a waffle explanation .. how about more general
> theoretical account of this phenomena?
Yep. This also seems very natural -- the more localized the (potential
and actual) effects, the easier to reason about (you can reason about
smaller chunks of code, so to say).

4;56 AM-ly yours,
Michael