[mercury-users] support for Prolog variables

[Fergus Henderson]

On 07-Sep-1998, Don Smith <dsmith at cs.waikato.ac.nz> wrote:
> The "NEWS" file for Mercury release 0.7.2 says
> 
>    * We have added some support for Prolog-style variables and coroutining.

Let me quote the complete item from the NEWS style:

 | * We have added some support for Prolog-style variables and coroutining.
 | 
 |   The module extras/trailed_updated/var.m provides a type `var(T)'
 |   which is a Prolog-style variable that holds a value of type T.
 |   These variables can have the new inst `any' described above.
 |   There's also an implementation of freeze/2, for coroutining
 |   (dynamic scheduling).  The extras/trailed_update/samples subdirectory
 |   has an example of the use of freeze/2 to solve the N-queens problem.

So note that you get Prolog-style variables only if you use this
new type `var(T)' and the new inst `any'.  This is quite intentional.

> Bravo!  Do you plan to support Prolog-style variables ("real" logical
> variables) wholeheartedly?  I hope so.

Well, I suppose that would depend on what you consider "wholeheartedly"
to mean.  Certainly we won't make `int' equivalent to `var(int)',
for example.

Prolog-style variables aren't very useful most of the time.
They can make programs harder to understand, they make static
checking difficult, and they can be very costly efficiency-wise.
So we certainly don't want them to be the default.

However, occaisionally you do want to do some constraint solving on
Herbrand terms.  We do want to have a solution for those relatively
rare occaisions, and that is what the `var' module is for.

We might well provide more direct support for this kind of thing at
some point in the future.  For example, we might one day allow some
kind of annotation on declarations for user-defined types to indicate
that values of that type may have inst `any'.  This would allow you to
use a type `foo' directly rather than using the type `var(foo)'; that
could improve efficiency as well as adding a little notational convenience.
(The HAL project, which is using Mercury as a target language, has already
given us some initiative in this direction, and indeed I believe that
Warwick Harvey was experimenting with a version of the Mercury compiler
modified along these lines.)
However, even if we do provide that kind of support,
the default would still be that user-defined types cannot have inst `any';
allowing inst `any' would remain an optional extra, not the default.

> Does this represent a change of direction for Mercury?

Not really.

Mercury has always had grand aims ;-)

Our plan was always to start with a small language, one that we
knew how to implement efficiently, and for which we could use static
checking to give strong compile-time guarantees, and to then gradually
extend it so that it could encompass a variety of different programming
techniques and paradigms -- while making sure that we didn't lose the
advantages of the original language.

For example, we started off with a purely static type system with no
capacity for dynamic typing.  For most programs, and certainly for most
parts of all large programs, static typing is exactly what you want.
Of course, you want your static type system to be as expressive as possible,
and towards that end we are extending the Mercury type system with
type classes and existential types.  However, for any given static
type system there may be some rare occaisions when you need to do
something that cannot be easily expressed within that system.
For this reason, long before we did anything with type classes and
existential types, we added support for the type `univ' and the
operations `type_to_univ' and `univ_to_type', which provide dynamic
type checking for those very rare occaisions when you need it.

> I'm curious to hear what made you support
> them.  Applications like unification grammars and theorem provers?

For constraint solving programs, it is clear that the modes cannot in
general be determined at compile time.  (Consider, for example,
a constraint `X = A * Y' over real numbers; if X and A are both ground,
then whether or not Y will become ground will depend on whether or not
A = 0, which in general cannot be determined at compile time.)
So, to support constraint solving, we added support for `any' insts.
`any' insts basically give you dynamic moding, just as the `univ'
type can provide dynamic typing.

Once we supported `any' insts for constraint solving, adding support
for Herbrand constraints -- that is, Prolog-style variables -- was a
relatively simple application of this.  (Well, maybe not *that* simple.
But simple enough and useful enough to be worth doing ;-)

Above I spoke about not losing the advantages of the original language.
I should elaborate on this a little.  Clearly if you're using dynamic
typing or dynamic moding, then you have lost some of the advantages
of the original completely statically typed and statically moded language.
So the point is not the ensure that you get all the original advantages
all the time; rather, you should get all the original advantages for
all the programs which you could write in the original language, and you
should get as many as possible of the original advantages for programs
which make use of the new feature.

Constraint solving and backtrackable destructive update both make
use of a trail, which is something that has "distributed fat" --
you pay an efficiency cost for the use of a trail even in code which
does not make use of it.  The principle of preserving the advantages of
the original language therefore lead us to make the use of a trail
optional -- programs which do not use it need not pay the price.

Committed choice nondeterminism is another example of a new feature
which also has a cost.  If you want to do concurrent programming, then
you need to have some sort of language support for committed choice
nondeterminism.  But committed choice nondeterminism can make programs
more difficult to reason about, more difficult to test, and more difficult
to debug.  Indeed, even there mere possibility of committed choice
nondeterminism can make programs more difficult to reason about.
In Mercury, we made committed choice nondeterminism an explicit part of
the statically-checked determinism system, so that you only get committed
choice nondeterminism if you have declared it, and so that you can tell
immediately from a predicate's declaration whether or not there is any
possibility of committed choice nondeterminism.  This ensures that you
only pay the costs of this feature if you use it.

I hope this helps to explain both our position on Prolog-style variables
and also the general philosophy behind the design of Mercury.

Cheers,
	Fergus.

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh>  |  of excellence is a lethal habit"
PGP: finger fjh at 128.250.37.3        |     -- the last words of T. S. Garp.