[m-dev.] Solver types: non-canonical types, `any' insts, equality

[Ralph Becket]

This is a "state of play" e-mail: after some animated HAL meetings and
vigorous e-mail exchanges, it is clear that solver types are subtle and
tricky things.  It seems that there is some disagreement ("Why on Earth
does it have to be that way/that complex/that cumbersome?") about the
design.  This e-mail is my attempt to explain the current design as I
see it.

If there really is a simpler design/way of doing things/view of the
problem then nobody would be happier to hear it than I.  (Thinking about
this stuff hurts your head.)



*** NEWSFLASH ***

I've just had a Glorious Revelation about how to handle these things
relatively painlessly.  The first part of this e-mail explains the
design as discussed on the mailing list and at the recent HAL meetings.
I think it is worth reading because IMHO it clearly explains what goes
on with non-canonical types, which, until my GR, were the source of
great grief.

The second, much shorter, part of this e-mail explains my GR which, I
think, addresses the problems we've been discussing.

*** END ***



DECONSTRUCTING NON-CANONICAL TYPES

[There's an illustrative example a little further down.]

The deconstruction of non-canonical types (i.e. ones with user-defined
equality) is tricky and is what makes things awkward.  The rule for
non-canonical types is:

	if a non-canonical type has more than one data constructor then
	it can only be deconstructed via an exhaustive switch which
	*must* succeed; the determinism of the switch is cc_multi.

This has caused some intense debate in the HAL meetings, but I
think I now understand enough to provide a convincing justification for
the rule.  

A value in a non-canonical type might have several equivalent
representations (e.g. with unordered lists denoting sets or with WAM
style variable chains.)  When we deconstruct a value of a non-canonical
type, conceptually the implementation "picks" (and commits to) one of
the possible representations of the value.

The implementation commits to the choice because it doesn't understand
equality for the type (equality is defined by a user-defined predicate),
hence the `cc_' part of the switch determinism.  (An awkardness of `cc_'
goals is that you cannot backtrack into them: all subsequent goals
*must* be guaranteed to succeed.  More on this later.)

The deconstructing switch has to be exhaustive for a similar reason.
The representation that the implementation commits to could conceivably
have at its top level any of the data constructors for the type.  An
inexhaustive switch might fail if it doesn't have a case for the
particular data constructor at the top of the committed-to value
representation.  But failing might be incorrect: it might be that there
are representations of the value being deconstructed that do start with
one of the data constructors included in the inexhaustive switch.

(Because the switch is exhastive and guaranteed to succeed, it has
determinism `cc_multi'.)

ILLUSTRATIVE EXAMPLE

The above is probably best illustrated with an example.  Consider the
definition

:- type t ---> f(int) ; g(string) ; h(t) where equality is eq.

We want to deconstruct a value X of type t so we use an exhaustive
switch:

	% VALID DECONSTRUCTION OF NON-FREE X
	%
	(	X = f(A), p1(...)
	;	X = g(B), p2(...)
	;	X = h(C), p3(...)
	)

At the start of the deconstructing switch the implementation commits to
a particular representation for the value of X (a handy optimization is
to use the one with which X was constructed :-) and we can efficiently
handle the deconstruction by matching the top-level data constructor of
the representation against one of the arms of the switch.

	% INVALID DECONSTRUCTION OF NON-FREE X
	%
	(	X = f(A), p1(...)
	;	X = g(B), p2(...)
	)

The problem with this piece of code is this.  At the start of the
deconstructing switch the implementation commits to a particular
representation for the value of X then tries to match the top-level data
constructor of the representation against one of the arms of the switch.
But this time disaster strikes!  The representation chosen this time is
h(f(123)) so a simple data constructor match won't tell us what arm of
the switch (if any) should be taken.
- We can't just fail because it might be the case that, say,
  eq(h(f(123)), f(123)).
- We can't start exploring all possible alternative representations for
  X because 
  - if there are an infinite number of them, none of which have f/1 or
    g/1 at the top-level, then this deconstruction may never terminate
  - and even if it could work, it would be a ridiculous strategy to
    pursue (hence the `cc_' designation.)
Put simply, there is no sensible way to work out which arm of the
disjunction should be taken or whether the disjunction as a whole should
fail.

SUMMARY

- Deconstruction of non-canonical values must be via exhaustive switch.
- These switches have determinism cc_multi.
- You cannot backtrack into a cc_multi goal, so it and the goals that
  follow must always succeed.

As I'll show later, together these things indicate that code
manipulating non-canonical values will be bulky and inelegant.


ANY INSTS AND SOLVER TYPE VALUES

If X has inst `ground' then the set u(X) of values that unify with X
forms an equivalence class - that is,

	all [Y, Z] ( Y in u(X), Z in u(X) => Y = Z )

If X has inst `any' then the set u(X) of values that unify with X does
not necessarily form an equivalence class.  That is, it may be the case
that

	some [Y, Z] ( Y in u(X), Z in u(X), Y \= Z )

In practice most solver type values are going to have inst `any'.

A solver type may use solver types in its data constructor fields.  For
example, the following Church numerals solver type is defined
recursively:

:- solver type church
	--->	zero
	;	succ(church)
	;	var(...)
	where initialisation is init, equality is eq.

When we deconstruct a succ/1 term (e.g. in the definition of eq/2) we
need the deconstructed argument to have inst `any' and not, say,
`ground' (it might not be ground according to the definition above.)
(Similar problems arise if we want to keep higher order arguments,
arrays, stores and other good things in solver type data constructors.)

To solve this problem we
- allow solver type definitions to include insts for data constructor
  fields;
- get the compiler to automatically generate an inst cast predicate for
  us.

So the right way to define church is

:- solver type church
	--->	zero
	;	succ(church `with_inst` any)
	;	var(...)
	where initialisation is init, equality is eq.

(fields without a `with_inst` annotation are assumed to be "naturally"
`ground') and the compiler constructs an inst cast predicate

:- impure pred 'inst cast church/0'(church, church).
:-        mode 'inst cast church/0'(in(any), out(<<i>>)) is det.
:-        mode 'inst cast church/0'(out(any), in(<<i>>)) is det.

where <<i>> stands for `bound(zero ; succ(any) ; var(ground))'.

Now we can use 'inst cast church/0'/2 to ensure that when we deconstruct
a succ/1 term its argument will have inst `any' as required.  (N.B. the
only way of going from <<i>> to `any' is via this inst cast predicate.)


DEFINING EQUALITY FOR THE CHURCH SOLVER TYPE

This is where things get rather awkward; I hope we can find a more
elegant solution.

Here's the code I wrote for equality for the church type:

:- pred eq(church::in(any), church::in(any)) is semidet.

eq(A, B) :-
		% This promises that the answer we get back from eq_2
		% really is the only one you can get, thereby converting
		% the call from cc_multi to det.  The unification then
		% changes det into semidet as required.
		%
	promise_only_solution(eq_2(A, B)) = yes.

:- pred eq_2(church::in(any), church::in(any), bool::out) is cc_multi.
:- pragma promise_pure(eq_2/3).

eq_2(A0, B0, Eq) :-
		% Make sure the only `var's we have to deal with are
		% at the end of any var chains.
		%
	impure deref(A0, A1),
	impure deref(B0, B1),

		% Do the inst cast so that deconstructions of succ/1
		% work properly.
		%
	impure 'inst cast church/0'(A1, A),
	impure 'inst cast church/0'(B1, B),

		% Exhaustive deconstruction switches on A then B.
		%
	( A = zero,    ( B = zero,    Eq = yes
	               ; B = succ(_), Eq = no
	               ; B = var(V),  Eq = yes, <<set V to A0>>
		       )
	; A = succ(C), ( B = zero,    Eq = no
	               ; B = succ(D), eq_2(C, D, Eq)
	               ; B = var(V),  Eq = yes, <<set V to A0>>
		       )
	; A = var(VA), ( B = zero,    Eq = yes, <<set VA to B0>>
	               ; B = succ(_), Eq = yes, <<set VA to B0>>
	               ; B = var(VB), Eq = yes, <<equate VA and VB>>
		       )
	).

[Now that, you have to admit, is quite a bit of work for a type with
just three data constructors...]

:- impure pred deref(church::in(any), church::out(any)) is cc_multi.

deref(A0, A) :-
	impure 'inst cast church/0'(A0, A1),
	(	A1 = zero,    A = A0
	;	A1 = succ(_), A = A0
	;	A1 = var(V),  <<extract A2 from V>>, deref(A2, A)
	).

Okay, the above works, but it's code that's 


HERBRAND TYPES

This is where things get really unpleasant and it illustrates the sort
of problem I expect solver type implementers will face frequently.

Let's say we plan to implement Herbrand types as a source-to-source
transformation.  We'll turn a definition like this

:- herbrand type t
	--->	a(...)
	;	b(...)
	...
	;	z(...)

into

:- solver type t
	--->	'$VAR'(wamvar(t))
	;	'$a'(...)
	;	'$b'(...)
	;	...
	;	'$z'(...)
	where initialisation is init_t, equality is eq_t.

- wamvar/1 is a private built-in polymorphic type implementing WAM-style
  variables;
- init_t/1 is defined for us by the compiler;
- eq_t/2 is defined for us by the compiler;
- somehow we've worked out which data constructor fields contain solver
  types and we've inserted the appropriate ``with_inst` any'
  annotations;
- every data constructor `a' has been renamed to `'$a'' and an extra data
  constructor `'$VAR'/1' has been introduced (I'm not suggesting `'$a''
  *be* the renaming, it's just meant to denote *a* unique renaming.)

Then we define eq_t/2 in a similar fashion to the way we did for Church
numerals (i.e. a big O(n^2) switch of switches).

Next we insert functions to handle construction and deconstruction for
`t'.  Here's how the (de)constructor function for data constructor `a'
might appear:

:- func a(<<ta1>>,      <<ta2>>,      ...) = t.
:- mode a(in(<<ia1>>),  in(<<ia2>>),  ...) = out(any) is det.
:- mode a(out(<<ia1>>), out(<<ia2>>), ...) = in(any) is semidet.

(<<ta1>> is the type of field 1 of `a', <<ia1>> is the designated inst
for field 1 of `a', and so forth.)

Then we implement the first mode (using Mercury's mode-specific
implementation syntax):

:- pragma promise_pure(a/<<arity of a>>).

a(X1::in(<<ia1>>), X2::in(<<ia2>>), ...) = (A::out(any)) :-
	impure 'inst cast t/0'(A, '$a'(X1, X2, ...)).

The reverse mode implementation seems neither elegant nor particularly
efficient:

a(X1::out(<<ia1>>), X2::out(<<ia2>>), ...) = (A::in(any)) :-
	promise_only_solution(a_2(A)) = yes({X1, X2, ...}).

:- pred a_2(A::in(any),
            maybe({<<ta1>>, <<ta2>>, ...)::
		out(bound(yes(<<ia1>>, <<ia2>>, ...)))
	   ) is cc_multi.

:- pragma promise_pure(a_2/2).

a_2(A0, Result) :-
	impure deref(A0, A1),
	impure 'inst cast t/0'(A1, A),
	(	A = '$VAR'(_),		Result = no
	;	A = '$a'(X1, X2, ...),	Result = yes({X1, X2, ...})
	;	A = '$b'(_, ...),	Result = no
	...
	;	A = '$z'(_, ...),	Result = no
	).

... and so on for each of the other data constructors.

Ouch.


THE GLORIOUS REVELATION

[I have yet to test this idea out, but I have a good feeling about
it...]

[Credit where it is due: upon reflection I think this is similar to what
Joachim was getting at.]

Let us revisit the Church numerals solver type, but this time I'm going
to use *two*: an "outer", non-canonical type, and an "inner" canonical
type.

Here's how it would look:

	% The "outer" type (non-canonical).
	%
:- solver type church ---> church(ch `with_inst` any)
	where initialisation is init_church, equality is eq_church.

	% The "inner" type (canonical).
	%
:- solver type ch ---> z ; s(church `with_inst` any) ; v(...)
	where initialisation is init_ch.

Now we define equality for church/0 like this:

:- pred eq_church(church::in(any), church::in(any)) is semidet.

eq_church(A0, B0) :-
	A = promise_only_solution(unwrap(A0)),
	B = promise_only_solution(unwrap(B0)),
	eq_ch(A, B).

	% Unwrap just strips off the `church' wrapper from a church/0
	% value.
	%
:- pred unwrap(church::in(any), ch::out(any)) is cc_multi.
:- pragma promise_pure(unwrap/2).

unwrap(Church0, Ch) :-
	impure 'inst cast church/0'(Church0, Church),
	Church = church(Ch).	% Valid because church/0 has only
				% one data constructor.  Even so, this
				% deconstruction is still cc_multi,
				% however.

	% Note, eq_ch/2 is *NOT* a definition of equality for ch/0.  It
	% is an auxiliary predicate used to define equality of church/0.
	%
:- pred eq_ch(ch::in(any), ch::in(any)) is semidet.
:- pragma promise_pure(eq_ch/2).

eq_ch(A0, B0) :-
	impure 'inst cast ch/0'(A0, A),
	impure 'inst cast ch/0'(B0, B),
	(
		A = z,
		B = z
	;
		A = s(C),
		B = s(C)
	;
		A = v(VA),
		...
	).

Et voila!  Equality with a linear number of cases.  Because the "inner"
type (ch/0) is canonical, virtually all the painful stuff goes away.

Moving on to code up the "outer" interfaces to the "inner" data
constructors, we define (de)constructor functions as follows:

:- func zero = (church::out(any)) is det.
:- pragma promise_pure(zero/0).

zero = Church :-
	impure 'inst cast ch/0'(Ch, z),
	impure 'inst cast church/0'(Church, church(Ch)).

:- func succ(church) = church.
:- mode succ(in(any)) = out(any) is det.
:- mode succ(out(any)) = in(any) is semidet.
:- pragma promise_pure(succ/1).

succ(Church0::in(any)) = (Church::out(any)) :-
	impure 'inst cast ch/0'(Ch, s(Church0)),
	impure 'inst cast church/0'(Church, church(Ch)).

succ(Church::out(any)) = (Church0::in(any)) :-
	impure 'inst cast church/0'(Church0, church(Ch0)),
	impure 'inst cast ch/0'(Ch0, Ch),
	Ch = s(Church).

And so on.  The code for the (de)constructor functions isn't pretty, but
it is efficient (the inst casts are essentially just variable renamings
and should be optimized away) and could potentially be simplified still
further.

That said, the bulk of the solver type implementation all happens at the 
"inner", ch/0 level, where there is no need for all that awkward mucking
about with cc_multi code and exhaustive switches.



What do you think?

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