[mercury-users] Impurity and foreign language calls
maclarty at cs.mu.OZ.AU
Wed Mar 15 10:35:18 AEDT 2006
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
> 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
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
> 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:
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 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.
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
More information about the users