[m-dev.] Revisiting `any' and inst casts for solver types

[Fergus Henderson]

On 30-Apr-2004, Ralph Becket <rafe at cs.mu.OZ.AU> wrote:
> Discussion in yesterday's HAL group meeting indicated that we may be
> able to do away with the need for inst casts with solver types.

In principle, I think you're right -- I think the original reason that
I didn't make any attempt to support deconstruction unifications for
variables with `any' insts in the mode checker is that the compiler didn't
know how such variables would be represented.  So long as you are willing
to pick a particular representation for such variables, I think there
should be no major obstacles to generating code for such unifications,
and so it should be OK to allow them in the mode checker.

However, the devil is in the details :)

Although I think it's OK to allow deconstruction unifications with `any' insts
in the mode checker, I'm not sure this will solve your problems -- see below.

> Going back to the Church numerals example, here's how things might look
> with "real" `any' insts:
> 
> 
> :- solver type church ---> church(ch)
> 	where initialisation is init, equality is eq.
> 
> :- type ch ---> z ; s(church) ; v(...).

What's in the "..."?

If the "..." is just "int", for example, as for the cfloat solver,
then there would be some potential problems.

In general the v(...) constructor used to represent partially instantiated
values is special, and probably ought to be treated specially in the
syntax and semantics.

In particular, normal constructors are mathematical functions, and
the composition of two mathematical functions is again a mathematical
function.  But if we consider the composition of church/1 and v/1,
we'll see that it is not a mathematical function.  In particular, if
the composition was a mathematical function then we would expect that
for any given (ground) X, the set of values that unify with church(v(X))
would form an equivalence class.  But this is not the case.

The issue is that the composition of church/1 and v/1 is not a
mathematical function from its arguments to church numerals; it can only
be considered as a function from the arguments *and the constraint store*
to church numerals.

-- 
Fergus Henderson                    |  "I have always known that the pursuit
                                    |  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
--------------------------------------------------------------------------