[m-dev.] Groundness for solver types

[Ralph Becket]

The solver types implementation progresses apace.  The issue I'm dealing
with now involves unification with inst `any' values; it's tricky enough
that I want to discuss it before proceeding.  Feedback is therefore most
welcome.

RETHINKING SOLVER TYPES (AGAIN...)

(Don't worry - what I'm proposing here is a relatively small change.)

Say we have a solver type for Church numerals:

:- solver type church
	--->	zero
	;	succ(church)
	where	constrained is
			var(church_var_repn `with_inst` church_var_inst),
		initialisation is init_church,
		equality is eq_church,
		comparison is cmp_church.

Here the `church' type has two ordinary data constructors, `zero' and
`succ/1', and one specially treated data constructor which I've called
`var/1'.

With what I've implemented to date, the compiler automatically
constructs a predicate for deconstructing `var/1' values

:- impure pred 'deconstruct var'(
			church::in(any),
			church_var_repn::out(church_var_inst)
		) is semidet.

and a function for constructing `var/1' values

:- impure func 'construct var'(church_var_repn::in(church_var_inst)) =
			(church::out(church_var_inst)) is det.

These are constructed specially partly because they involve inst casts.
They are impure because they allow one to observe the "boundness" of a
value.

Next we want to define eq_church, the user-defined equality predicate,
and this is where the current batch of problems begin.

:- pred eq_church(church::in(any), church::in(any)) is semidet.
:- pragma promise_pure(eq_church/2).

eq_church(A, B) :-
	A = succ(C), B = succ(C).

eq_church(A, B) :-
	A = zero, B = zero.

eq_church(A, B) :-
	( if impure 'deconstruct var'(A, AVarRep) then
		( if impure 'deconstruct var'(B, BVarRep) then
			...
		  else
		  	...
		)
	  else
	  	impure 'deconstruct var'(B, BVarRep) then
	  	...
	).

At this point the compiler whinges that

church.m:054: In clause for `eq_church(in(any), in(any))':
church.m:054:   mode error in unification of `A' and `church.succ(C)'.
church.m:054:   Variable `A' has instantiatedness `any',
church.m:054:   term `church.succ(C)'
church.m:054:   has instantiatedness `church.succ(free)'.

Part of the problem is that the compiler doesn't know how to deconstruct
inst `any' values.

One way around the problem would be to do away with
`'construct ...'' and `'deconstruct ...'' and instead have the compiler
automatically define an inst cast function like this:

:- impure func 'inst cast church/0'(church) = church.
:-        mode 'inst cast church/0'(in(any)) =
			out(bound(	zero
				;	succ(any)
				;	var(church_var_inst)
			)) is det.
:-        mode 'inst cast church/0'(out(any)) =
			in(bound(	zero
				;	succ(any)
				;	var(church_var_inst)
			)) is det.

We could then write

eq_church(A0, B0) :-
	impure A = 'inst cast church/0'(A0),
	impure B = 'inst cast church/0'(B0),
	( if A = var(AVarRep) then
		...
	  else if B = var(BVarRep) then
		...
	  else
		(
			A = succ(C), B = succ(C)
		;
			A = zero, B = zero
		)
	).

and (hopefully) all would be well.

There are some difficulties here.

The final inst I used for the argument of `'inst cast church/0'' was

	bound(zero ; succ(any) ; var(church_var_inst))

Presumably if I had defined `church' as

:- solver type church
	--->	zero
	;	succ(church)
	;	foo(string)
	where	constrained is
			var(church_var_repn `with_inst` church_var_inst),
		...

the final inst would have been

	bound(zero ; succ(any) ; foo(ground) ; var(church_var_inst))

What if, instead of `foo(string)', the constructor was `foo(array(char))'
or `foo(pred(int))' and we want more useful insts than `ground' for the
argument of `foo/1'?

What if `church' was a parametric type:

:- solver type church(T)
	--->	zero
	;	succ(church)
	;	foo(T)
	where	constrained is
			var(church_var_repn `with_inst` church_var_inst),
		...

What should the final inst be now?  The type `T' may or may not be a
solver type.

Right now we don't have any good way of connecting `any' to an
expressive set of underlying insts.

My idea for the first version of solver types is to allow the programmer
to explicitly associate insts with constructor fields in a solver type.
That is, rather than writing

:- solver type church
	--->	zero
	;	succ(church)
	;	foo(string)
	;	bar(array(char))
	where	constrained is
			var(church_var_repn `with_inst` church_var_inst),
		initialisation is init_church,
		...

one would write

:- solver type church
	--->	zero
	;	succ(church `with_inst` any)
	;	foo(string)
	;	bar(array(char) `with_inst` uniq_array)
	;	var(church_var_repn `with_inst` church_var_inst)
	where	initialisation is init_church,
		...

With this scheme
- there is no `constrained is special_ctor' where-attribute;
- insts are explicitly associated with constructor fields (a default
  inst of `ground' is assumed for fields without inst annotations);
- the user can specify precise insts for all fields and also for
  polymorphic fields (this at least allows the programmer to say
  whether a particular polymorphic field is expected to be a solver
  type or not);
- instead of `'deconstruct special_ctor'' and `'construct special_ctor''
  the compiler just generates `'inst cast church/0'' for us;
- there is no need to do a pass removing `'deconstruct special_ctor''
  and `'construct special_ctor'' calls for switch detection to work;
- the existing Mercury code for constructions and deconstructions
  doesn't need to be changed.

The down side is that we can only have one inst associated with each
constructor field.  I think this is probably livable in practice and can
also probably be relaxed in a future design if necessary.

SOLVER TYPES IN NON-SOLVER CONTAINER TYPES

While I'm on the subject, I think it should be a compile-time error to
implicitly inst cast from `any' to `ground'.  For instance, I think the
following is wrong:

:- pred baz(T::in(any), T::in(any), {T, T}::out) is det.
baz(X, Y, {X, Y}).

Why?  Because the set of values unifiable with a `ground' value must
form an equivalence class, whereas the set of values unifiable with
an `any' value might not form an equivalence class.  Therefore,
implicitly casting from `any' to `ground' (as in `baz/3' above) is not
sound.

UNIFICATION MORE GENERALLY

The Mercury compiler will use inst information to decompose a
unification into deconstructions as far as possible.  A call to
`builtin.unify/2' or a type-specific unification predicate is used to
handle ground/ground unifications.

`builtin.unify/2' has the signature below, as do mode 0 procedures for
compiler-generated type-specific unification predicates (the compiler
may opt to generate other procedures for type-specific unifications that
cannot be decomposed into deconstructions, but which are have more
specific insts than ground/ground.)

:- pred builtin.unify(T::in, T::in) is semidet.

This won't work when the arguments have inst `any'.

What should happen when one or both arguments have inst `any'?  For
any/any unifications we could add an extra mode to `builtin.unify/2':

:- mode builtin.unify(T::in(any), T::in(any)) is semidet.

I don't see any immediate problem here.

What about any/non-any unifications?  It occurrs to me that this cannot
happen in the polymorphic case because otherwise the non-any inst would
give us compile time knowledge of the type of the type parameter!
Therefore we must know the type for an any/non-any unification.  I
propose that in this case
- if the non-any inst is a subinst of the solver type inst then we
  just cast that argument to `any' and call `builtin.unify/2' (or the
  type-specific unification predicate);
- if the non-any inst is not a subinst of the solver type inst then we
  report an error.

That is,

	% X `with_type` church `with_inst` bound(zero ; succ(any))
	% Y `with_type` church `with_inst` any
	X = Y

is compiled as

	some [X1] (
		impure 'inst cast church/0'(X1) = X,
		builtin.unify(X, Y)	% or eq_church(X, Y)
	)

whereas

	% X `with_type` church `with_inst` bound(zero ; succ(ground))
	% Y `with_type` church `with_inst` any
	X = Y

is reported as an error by the compiler.  Does anybody see any problems
with this?  Does anybody have a better idea?

DECONSTRUCTION OF NON-CANONICAL TYPES

What about the restrictions placed on non-canonical types?  The main
problem I see is that deconstructions that can fail are not permitted
for such types.

One option is to simply initialise a new variable for each field of a
"deconstructor" and then do a general unify in this case.

That is, compile

	% X `with_type` church `with_inst` any
	% Y `with_inst` free
	X = succ(Y)

as

	init_church(Y),
	some [Tmp] (
		Tmp = succ(Y),		% Construction
		builtin.unify(X, Tmp)
	)

This isn't going to win any prizes for efficiency, but does give us the
sort of freedom we need (imagine trying to use Herbrand types without
it...)

Any objections?

I'd very much like to hear people's thoughts about these matters.

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