[m-dev.] Revisiting `any' and inst casts for solver types
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
> 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
Otherwise, everything is much the same as before.
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