[mercury-users] Request for comments on this code

[Peter Schachte]

On Wed, Jul 12, 2006 at 01:47:33PM +1000, Ian MacLarty wrote:
> On Wed, Jul 12, 2006 at 11:04:23AM +1000, Peter Schachte wrote:

> > so the IO state needs to be threaded through ...
> > everything that could make an observable change to the state
> > of the world.
> 
> No I disagree.  You could measure the effect of calling the procedure:
> 
> 	do_something(T::in, T::out) is det
> 
> without threading the IO state through it as follows:
> 
> get_time(T0, !IO),
> make_input(In, !IO),
> do_something(In, Out),
> consume_output(Out, !IO),
> get_time(T, !IO)

If do_something/2 has an (out, out) mode, or if consume_output has an
(in, di, uo) mode, that's not true.  And anyway, this is a pretty
artificial example.  Yes, if you're very careful about modes, and know
a lot about how the current release of the Mercury compiler reorders
goals for the compilation model you've chosen, you can have a pretty
good idea of the semantics of your code.  But I don't think you
should have to know those things to understand the denotation of your
code.

> My beef is with your argument that the IO state cannot contain things
> that might be affected by the running of non-IO procedures in the
> program.  Trying to work out what things can be affected by the running
> of the program and what things can't is an impossible task.

Yes, that's true.  The thermometer and swap file size examples suggest
that I need to soften my statement a little.  The question is the
programmer's intent.  When I read a thermometer or swap file size, am
I measuring the world outside my program, where I don't care about the
effect of parts of my program on the value I read, or do I care?  If
I'm trying to measure the effect of big_hulking_non_io_goal/0 on the
size of my swap file, then I need to either make the code to read the
swap file size impure, or thread the IO state through
big_hulking_non_io_goal/0.  Failing to do so leaves the declarative
semantics of my program as the mercy of the whims of the compiler.
And I would argue that threading the IO state through
big_hulking_non_io_goal/0 without ever using it isn't right either,
because I'd like the compiler to have the right to remove unneeded
arguments.  So inspecting the state of the world with a threaded IO
state is declaratively fine, provided you're not using it with the
intention of measuring an effect of Mercury code that does not thread
the IO state.

> Do you agree that trying to exclude things that might be affected by the
> running of the program from the IO state is ridiculous?

That's a bit more extreme than I'm arguing.  I'm saying we should not
notionally include things in an IO state that can be changed by goals
that do not thread the IO state, if we mean to use them to measure the
effects of Mercury code.  This will hardly ever come up other than in
benchmarking.  And whether or not it's ridiculous is immaterial.  I
don't see any declarative alternative.

> All I'm proposing is an interpretation of the IO state that allows
> things that can be affected by the running of the program to also be in
> the IO state.  So far I've had no problem with this interpretation.

The problem is that Mercury can reorder goals such that you're not
measuring what you think you're measuring.  You've argued that in
certain cases you can practically force a goal ordering without using
the IO state, but that doesn't mean you have a declarative reading.
Generally Mercury takes the view that constructs that aren't always
declarative are impure.  get_clock(Time, !IO) isn't always
declarative.

-- 
Peter Schachte              If your thesis is utterly vacuous Use
schachte at cs.mu.OZ.AU        first-order predicate calculus. With sufficient
www.cs.mu.oz.au/~schachte/  formality The sheerist banality Will be hailed
Phone: +61 3 8344 1338      by the critics: "Miraculous!" -- Anon. 
--------------------------------------------------------------------------
mercury-users mailing list
post:  mercury-users at csse.unimelb.edu.au
administrative address: owner-mercury-users at csse.unimelb.edu.au
unsubscribe: Address: mercury-users-request at csse.unimelb.edu.au Message: unsubscribe
subscribe:   Address: mercury-users-request at csse.unimelb.edu.au Message: subscribe
--------------------------------------------------------------------------