[m-dev.] Solver types in Mercury - meeting notes and comments

[Fergus Henderson]

On 12-Feb-2004, Ralph Becket <rafe at cs.mu.OZ.AU> wrote:
> This is partly a review of the HAL/Mercury meeting held on Thursday 12
> February on adding solver types to Mercury, and partly personal
> comment/suggestion.
...
> I have
> probably put `is semidet' where there should be `is cc_multi' for the
> equality predicates and missed off the odd promise_only_solution
> wrapper, but hey, that's minor detail.  I hope!]

I think some of those details are pretty important :)

> SOLVER TYPES
...
> One issue is that while users of a solver type will see its values as
> having inst any, the solver implementation will need more refined inst
> information.  Some inst casting is required and there is a question as
> to how and where this should happen.

It's not just inst casting that is required.  You need to do type casting
at the same time.  For a solver type, there is an important distinction
between the set of (ground) values of the solver type, and the set of
representations (values of the solver's *representation* type), which
may represent constrained non-ground values.

> SUGGESTION
> 
> This was not discussed in the meeting, but I think it summarises where
> we had got to in our thinking when the meeting broke up.
> 
> Consider the solver type t which I'll define using some hypothetical
> syntax:
> 
> :- solver type t ---> v(u `with_inst` i) ; a ; b(t) ; c(int) ; d(cfloat)
> 	where initialisation is init_t, equality is equal_t.
> 
> What does this mean?  (I'll come to the `where ...' part in a bit.)

Good question.  But I'm still waiting for the answer :)
I would like to know the declarative semantics, not just the
operational semantics.  In particular, what is the set of (ground) values
for the type, and what are the equality axioms?

In general, it is strongly preferable if all Mercury constructs can be
given both a declarative semantics and an operation semantics, and for
the operational semantics to be sound w.r.t. that declarative semantics.
I am not yet convinced that that is the case for your proposal.

> :- solver type cfloat ---> cf(float `with_inst` ground)
> 	where initialisation is init_cfloat, equality is equal_cfloat.

What is the set of ground values for this type?

> :- pred init_cfloat(cfloat::out(any)) is det.
> :- pragma promise_pure(init_cfloat/1).
> 
> init_cfloat(cf(Id)) :-
> 	impure <<construct a new, initialised constrained integer,
> 		give it an float identifier, and assign it to Id>>.

Did you mean to say

 	impure <<construct a new, initialised constrained float,
 		give it an int identifier, and assign it to Id>>.

?

Wouldn't that be a type error, since the argument of cf/1 has type
`float', not `int'?  Did you mean to write

	:- solver type cfloat ---> cf(int `with_inst` ground) where ...
	                              ^^^
?

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
The University of Melbourne         |  of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh>  |     -- the last words of T. S. Garp.
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------