[m-dev.] higher order types, overloading

[Mark Brown]

Hi all,

The implementation of constructor classes raises some language design
issues, one of which I thought I'd bring up now in case anyone wants to
comment.  The issue is how to resolve overloading of type names with
different arities, given that type expressions will no longer have to
have all arguments supplied.

For example, given the declarations:

	:- type pair(A, B) ---> A - B.
	:- type pair(A) == pair(A, A).

how do we know whether the type expression pair(int) should have kind `*'
or kind `* -> *'?

The general solution is to use kind inference to determine the correct kind
from the context: if the expression appears where kind `*' is expected then
it is referring to pair/1, and if it appears where kind `* -> *' is expected
then it is referring to pair/2.

There are two problems with this, one from an implementation point of view,
and one from a language design point of view.

The implementation problem is that we do module qualification and expanding
of equivalence types very early in the compilation process -- earlier than
I was planning to place kind inference -- so there is no way to resolve the
overloading when it is needed to be resolved.  This problem is not
insurmountable: conceivably the expanding of equivalence types could be left
until later (possibly not a bad idea anyway), and module qualification of
such cases could be delayed until enough kind inference has been done
(similarly to how we delay module qualifying calls until enough type
inference has been done).

The language design issue is that programs that make heavy use of this form
of overloading, while they may be cute, are likely to be quite difficult to
understand.  I'd be very much inclined to force users to avoid such
overloading, or at least force them to use kind annotations, to avoid this
problem.  IMHO this is not too much price to pay.

So, rather than implement the general solution mentioned above, here's
what I propose.  The correct arity for a given type constructor should be
found by attempting the following rules in the order given:

	1) If there is an explicit kind annotation, use that to determine
	the arity of the type constructor.

	2) If there is only one possible match, use that.

	3) If there is an exact match (that is, if we have supplied N
	arguments and there is a symbol defined with N parameters), use
	that.  In other words, if we can give the type expression kind `*'
	then we do.

	4) Report an ambiguity error, and suggest that the user use kind
	annotations to resolve it.  That is, if we have a choice between
	`* -> *' and `* -> * -> *', we don't favor either choice.

We would be able to implement these rules as part of the module qualification
pass, and leave full kind inference until later.  Doing this will also
simplify kind inference since there will be no disjunctive constraints on the
kinds -- all choices will have already been made.

Two possible variations:

	- As above, but leave out rule 3.  IMHO rule 3 should stay, since
	kind `*' would be by far and away the most common case, and would
	be what readers of the code would naturally expect when they see
	a type expression.

	- As above, except that in rule 4 choose the simplest kind, for some
	value of "simplest".  For example, choose the kind with the shortest
	left-hand branch (that is, choose the arity which is closest to the
	number of arguments supplied).  IMHO, this would be giving users too
	much rope.

Any comments?

On a related note, I don't plan to allow any new sorts of overloading.  In
particular, overloading on arity will not be extended to overloading on
kind, even though it would be technically possible.  For example, although
we allow the type `pair' to be defined twice as long as the arities differ,
we will not allow the type `foo/3' to be defined twice even if the kinds
of the arguments differ.

The rationale for this is that allowing this form of overloading would
raise a similar language design issue as that mentioned above, only much
worse.

Also, I don't plan to allow polymorphic kinds (for example, kinds such as
`all [K] (K -> *) -> K -> *'), at least not until I become aware of a good
reason to allow them.  After kind inference, any remaining kind variables
will be bound to `*'.  Likewise, kind annotations will have to be ground.
You either have to give the complete kind, or give nothing at all.

Cheers,
Mark.

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