[mercury-users] higher-order programming

[Fergus Henderson]

On 22-May-2005, Peter Ross <pro at missioncriticalit.com> wrote:
> Can someone please remind me why it's not possible to write the
> following program, instead one must use the commented out line.
> 
> :- pred p(int::out) is det.
> 
> p(X) :-
>         F = f(1),
>         G = F(2),
>     	% G = (func(X1) = F(2, X1)),

When the Mercury type checker was originally written, it did not
support type classes.  If you think about the type checker as a
constraint solver, it did not support any delayed constraints;
all constraints were evaluated eagerly.  Disjunctive constraints -- as
can arise with overloading -- were (and still are) handled by forking
the whole constraint store.

The difficulty with typing "G = F(2)" is that there is an _infinite_
family of solutions to that typing constraint:

	{ G :: T1,                F :: func(int) = T1 }, 
	{ G :: func(T1) = T2,     F :: func(int, T1) = T2 }, 
	{ G :: func(T1, T2) = T3, F :: func(int, T1, T2) = T3 }, 
	...

Obviously you can't handle this infinite overloading by eagerly
forking an infinite number of copies of the constraint store.

Now that we have support for type class constraints, it might
be possible to handle this more nicely.  We could add a
built-in type class constraint "apply(T1, T2, T3)" which
is satisfied iff "X1 = X2(X3)" is well-typed where
X1 has type T1, X2 has type T2, and X3 has type T3.
Similarly the type class constraint "apply(T1, T2, T3, T4)"
would be satisfied iff "X1 = X2(X3, X4)" is well-typed where
each X_i has type T_i (for i in 1 to 4), and likewise for higher arities.

Then when the type checker sees 'Y = F(X)', instead of inferring
the type assignment

	{ F :: func(T1) = T2, X :: T1, Y :: T2 },

it would infer the constrained type assignment

	{ F :: T1, X :: T2, Y :: T3 <= apply(T1, T2, T3) }.

There would need to be some built-in rules for simplifying
type class constraints for this built-in type class, in
particular simplifying away constraints of the form "apply(T1, ...)"
when the top-level functor of T1 is known.

**********

In the mean time, a work-around is to use a user-defined
type class, with a functional dependency:

	:- typeclass my_apply(T1, T2, T3) <= (T1 -> T2, T3) where [
		my_apply(T1, T2) = T3
	].

	:- instance my_apply(func(T1) = T2, T1, T2) where [
		my_apply(F, X1) = F(X1)
	].
	:- instance my_apply(func(T1, T2) = T3, T1, func(T2) = T3) where [
		my_apply(F, X1) = (func(X2) = F(X1, X2))
	].
	:- instance my_apply(func(T1, T2, T3) = T4, T1, func(T2, T3) = T4)
	where [
		my_apply(F, X1) = (func(X2, X3) = F(X1, X2, X3))
	].
	% ... etc. (add as many instances as you need).

Then instead of using "G = F(2)", you could use "G = my_apply(F, X)".

Well, that would be a work-around, if only it was allowed!
Currently I get error messages for the instance declarations:

	Error: expected type in instance declaration to be a functor with
		variables as args: (func _1) = _2.
	Error: expected type in instance declaration to be a functor with
		variables as args: func(_1, _2) = _3.
	Error: expected type in instance declaration to be a functor with
		variables as args: func(_1, _2, _3) = _4.

That looks like a bug to me; higher-order function types ought to be allowed
in those positions.

-- 
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-users mailing list
post:  mercury-users at cs.mu.oz.au
administrative address: owner-mercury-users at cs.mu.oz.au
unsubscribe: Address: mercury-users-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-users-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------