[m-dev.] higher order types, overloading

[Mark Brown]

On 13-May-2005, Ralph Becket <rafe at cs.mu.OZ.AU> wrote:
> Mark Brown, Friday, 13 May 2005:
> > 
> > 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.
> 
> I have no problem with adding explicit kind annotations in the few
> places I need them (will it be mainly instance declarations for type
> classes using constructor classes?).

Kind annotations should be allowed anywhere a type expression with kind
other than `*' is allowed, including in the arguments to type constructors
in type expressions.  The reason for this is to allow users to overcome
the error reported by rule 4, below.  Kind annotations will also be allowed
on the parameters of type and typeclass declarations.  Conceivably we could
allow kinds to be specified in quantifier lists, although I don't plan to
implement that right away, since it isn't necessary.  (For example, you
might want to write "some [A `with_kind` (t -> t), B] pred ...".)

The place where kind annotations are truly necessary is in abstract type
and typeclass declarations.  Without them, constructor classes could not
in general be abstractly exported without breaking the abstraction barrier.

> 
> Overloading on arity is, I think, a real aid to program readability when
> used appropriately.  I would be loath to forbid it (it would break heaps
> of code).

We won't be forbidding it, and all current programs will continue to work
fine due to rule 3 below, since all current type expressions have kind `*'.

Currently you can look at a type constructor and the number of arguments
applied to it and know exactly what the sym_name_and_arity should be,
without looking at the context.  Same goes for data constructors.  Same
does not, however, go for predicates and functions, where you can create
a higher order term by the simple expedient of not supplying all the
arguments.  The consequence is that, if that predicate or function name is
overloaded, you need to look at the context to figure out what the real
arity of the symbol is, and even then it can still be ambiguous.  If we
always required the use of an explicit lambda quantiifier, then this
ambiguity would never arise.

You can think of kind annotations as being like a limited form of lambda
expression for constructing higher order types.  For example:

	Expr `with_kind` (t -> t)

means something like

	lambda [T] apply(Expr, T)

where the meaning of apply should be obvious.

So, when I said "this form of overloading" above, what I really meant is the
use of an implicit lambda quantifier for type expressions, much as you can
have an implicit lambda quantifier for term expressions by not supplying all
the arguments to a function or predicate.  I don't think this should be
allowed for types; higher order types are not likely to be used as often as
higher order terms, and they are not likely to be as cumbersome when they
are, so I don't think that the shorthand form is justified -- particularly
given the ambiguity that can arise as a result.

In other words, type constructors will continue to be treated like data
constructors, not like predicate and function names.

In any case, we can always decide to allow this shorthand in future if it
really is warranted.  We wouldn't be so easily able to take it away.

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