[mercury-users] Impurity and foreign language calls

[Ian MacLarty]

On 14 Mar 2006, at 23:04, doug.auclair at logicaltypes.com wrote:

> Dear all,
>
> I'm interacting with a third-party C-API, which has me declaring
> the Mercury proxies as impure, where I think the declaration is
> meritted.
>
> The problem is that impurity seems to taint the callers, too, and
> I'm wondering how to limit this damage.
>
> For example, let's say I have a digital camera with the C-API
> to control the hardware (taking and storing the image, firing
> the flash) and to read the battery power remaining.
>
> :- impure func battery_power = float.
>
> is the proxy to the C-API call.  Is this correctly declared
> impure?

Yes, but you could make it pure by declaring it as:

:- pred battery_power(float::out, io::di, io::uo) is det.

This seems to be the right thing to do here, since you're interacting 
with the outside world (i.e. the camera).  If you reflect this fact in 
the declarative semantics, using the abstract io.state arguments, then 
it needn't be impure.

> I get a different answer each time I call it, depending
> on previous explicitly unrelated (but implicitly related)
> calls (take_picture, discharge_flash).
>
> If battery_power must be impure, is there a way to make
> callers to it pure?  For example, I have:
>
> :- type battery_state ---> battery_state(availibility, min_charge).
> :- type availibility ---> ready; recharging.
> :- type min_charge ---> minimum(float).
>
> :- impure pred update_battery_state(battery_state, battery_state).
> :- mode update_battery_state(in, out) is det.
> update_battery_state(battery_state(_, minimum(X)), NewState) :-
>   impure Power = battery_power,
>   (Power > X -> Readiness = ready; Readiness = charging),
>   NewState = battery_state(Readiness, minimum(X)).
>
> Is update_battery_state pure, even though it calls battery_power?

Yes.  The reason it is impure is because you may get different outputs 
for the same inputs.  Adding a pair of io.state arguments will solve 
this.

> If not, would writing a C wrapper to the external calls that
> embed battery charge into the called and returned values (state
> variables for C, as it were), and have that wrapper make the
> battery power call internally, would that C wrapper (and other
> like-kind C wrappers for take_picture and discharge_flash) then
> be pure?
>

I don't think so.  The only way to make it pure would be to add a pair 
of io.state arguments, since you're doing I/O.

When considering if something is pure or not you need to consider 
whether the predicate is true for the same set of argument values 
throughout the lifetime of the program (or, more formally, that it is 
always true for the same set of ground atoms).  In your example the 
following atom may be true at some point in the program's execution, 
but false at a later point:

update_battery_state(batter_state(charging, minimum(0.5)),
	batter_state(ready, minimum(0.5)).

depending on the value returned by battery_power when it is called.  
This means it must be impure.

By adding a pair of io.state arguments, the output of 
update_battery_state also depends on the state of the world (including 
the camera), so it will always give the same results for the same 
inputs (since the state of the world will be an input).

You also need to consider whether a predicate has side effects when 
deciding if it is impure.  For example you may have the following 
impure predicate:

:- impure pred impure_print(string::in) is det.

that writes a string to stdout.  Even though the atom impure_print(S) 
is true for every value of S (and therefore true for the same set of 
ground atoms throughout the lifetime of the program), it is still 
impure since it updates state not reflected in it's arguments.

I think it is worth noting that it hasn't been well defined exactly 
what state can be updated by a pure predicate and not reflected in its 
arguments (or at least I'm not aware of any such definition).  For 
example all predicates update the stack pointer and possibly the head.  
These are not reflected in their arguments, but not all predicates are 
impure.  Also predicates that use solver_types and any insts update a 
global constraint store that is not reflected in their arguments, yet 
they too are allowed to be pure.

Ian.

--------------------------------------------------------------------------
mercury-users mailing list
post:  mercury-users at cs.mu.oz.au
administrative address: owner-mercury-users at cs.mu.oz.au
unsubscribe: Address: mercury-users-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-users-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------