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

Ralph Becket rafe at cs.mu.OZ.AU
Tue Jun 1 10:27:10 AEST 2004

Fergus Henderson, Tuesday,  4 May 2004:
> 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 [...]

Thanks for the feedback!  I'm very keen that we have a sound story to
tell about solver types.

Having thought about this some more, once we introduce solver types we
*can't* have a simple propagation of the form `any' means "bound to a
constructor, all of whose fields have inst `any'", nor can we say that
`ground' means "bound to a constructor, all of whose fields have inst

The show-stoppers are that
(1) a `ground' solver value may be composed of non-ground values (e.g. a
solver int represented as the difference of two other solver ints - the
difference may be known, but the values of the solver ints in the
difference may not);
(2) an `any' value's representation may well include `ground' terms, but
we cannot easily cast from `any' to `ground'.  Making this cast type
dependent (i.e. solver vs non-solver) is difficult and anyway does not
seem to solve the problem in the general case.

[I posted about this problem to the HAL mailing lists, but forgot to Cc:
the Mercury developers.  I've since forwarded that e-mail to the Mercury
developers list.]

> However, the devil is in the details :)

Tell me about it...

> > 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.

That's what I had in mind for "...".

> 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.

Yes: if "ground X" => "ground v(X)" then you are correct.  

So the question is, can we tell a story for solver types where the
implication doesn't hold in general?  Having spent a day scratching my
head, I don't think we can get away with that.

So here's yet another suggestion.  We start with some syntax like this:

:- solver type <<solver type name and params>>
	where	representation is <<representation type name and args>>,
		ground         is <<ground inst>>,
		any            is <<any inst>>,
		equality       is ...

This says that
- <<solver type>> is implemented using <<representation type>>,
- a `ground' <<solver type>> value has a corresponding <<ground inst>>
  <<representation type>> value,
- an `any' <<solver type>> value has a corresponding <<any inst>>
  <<representation type>> value.

Going back to the Church numerals example:

:- solver type church
	where	representation is ch,
		ground         is ground_ch,
		any            is any_ch,
		equality       is equal_church.

:- inst ground_ch == ...
:- inst any_ch    == ...

The compiler will treat `church' as an opaque foreign type and will
construct a predicate to handle conversion between `church' and its
internal representation `ch':

:- impure pred 'church/0 representation'(church,   ch            ).
:-        mode 'church/0 representation'(in(any),  out(any_ch)   ) is det.
:-        mode 'church/0 representation'(out(any), in(any_ch)    ) is det.
:-        mode 'church/0 representation'(in,       out(ground_ch)) is det.
:-        mode 'church/0 representation'(out,      in(ground_ch) ) is det.

This approach doesn't require any special new syntax apart from the
solver type definition and having the impure predicate for casting
between the solver-type view and the representation-type view means
we don't have problems with the interpretation of data constructors
as functions.

Otherwise, everything is much the same as before.

-- Ralph
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

More information about the developers mailing list