How to generate lists of fresh variables in Mercury like I can in Prolog?

Question

In SWI Prolog, list(Xs) :- length(Xs, _). is "pure" in that I can pass it a variable with any sort of instantiatedness and it will nondeterministically unify it with all most general unifiers of a particular length.

Is it possible to write a pure list/1 in Mercury? The manual seemed to hint this could be done, but I'm having trouble actually implementing it.

What I have so far is:

:- module mylist.

:- interface.

:- import_module list.

:- inst frees for list/1
    --->    []
    ;       [free | frees].
:- mode free_to_frees == free >> frees.

:- pred mylist(list(_)).
:- mode mylist(in) is det.
:- mode mylist(free_to_frees) is multi.

:- implementation.

:- pragma promise_pure(mylist/1).

mylist(_::in).

mylist([]::free_to_frees).
mylist([_|Xs]::free_to_frees) :- mylist(Xs).

However, when I try this:

:- module main.
:- interface.
:- implementation.
:- import_module list, mylist.

:- pred getlist(list(int)).
:- mode getlist(free >> ground) is multi.
getlist(Xs) :- Xs = [1, 2, 3].
getlist(Xs) :- mylist(Xs), Xs = [5].

I get the following error:

main.m:011: In clause for `getlist(out)':
main.m:011:   mode error in conjunction. The next 2 error messages indicate
main.m:011:   possible causes of this error.
main.m:011:   
main.m:011:   In clause for `getlist(out)':
main.m:011:   mode error in unification of `Xs' and `list.[V_10 | V_16]'.
main.m:011:   Variable `Xs' has instantiatedness
main.m:011:     bound(
main.m:011:       []
main.m:011:     ;
main.m:011:       '[|]'(
main.m:011:         free,
main.m:011:         named inst mylist.listskel,
main.m:011:         which expands to
main.m:011:           bound(
main.m:011:             []
main.m:011:           ;
main.m:011:             '[|]'(
main.m:011:               free,
main.m:011:               named inst mylist.listskel
main.m:011:             )
main.m:011:           )
main.m:011:       )
main.m:011:     ),
main.m:011:   term `list.[V_10 | V_16]' has instantiatedness
main.m:011:   `named inst list.'[|]'(unique(5), free)'.
main.m:011:   
main.m:011:   In clause for `getlist(out)':
main.m:011:   in argument 1 of clause head:
main.m:011:   mode error in unification of `HeadVar__1' and `Xs'.
main.m:011:   Variable `HeadVar__1' has instantiatedness `free',
main.m:011:   variable `Xs' has instantiatedness
main.m:011:     bound(
main.m:011:       []
main.m:011:     ;
main.m:011:       '[|]'(
main.m:011:         free,
main.m:011:         named inst mylist.listskel,
main.m:011:         which expands to
main.m:011:           bound(
main.m:011:             []
main.m:011:           ;
main.m:011:             '[|]'(
main.m:011:               free,
main.m:011:               named inst mylist.listskel
main.m:011:             )
main.m:011:           )
main.m:011:       )
main.m:011:     ).

I'm guessing my use of free may be incorrect, or else I need to add an additional mode or generalize my listskel inst to cover the case of mylist(Xs), Xs = [5].

Basically, how should I write mylist/1, so that it can be used in as many modes as possible?

Thank you!

Answer 1

Due to a limitation in the Mercury implementation, which is documented in the LIMITATIONS file in the Mercury distribution, what you ask for cannot be done.

While the design of the Mercury language allows modes that describe partially instantiated terms such as a list of free variables, such as the intended output of mylist(Xs), such terms are not useful unless you can do something with them, such as unify them with [5]. Since the Mercury compiler needs to know the instantiation state of all variables at all program points, it can allow this only if it can keep track of all unifications between free variables in such terms with other free variables (whether they occur in such terms or not). This is because if you have unifications A = B, B = C, and C = D, and then you unify D with 5, the compiler needs to know that this grounds not just D, but A, B and C as well. This is because those unifications have made A, B and C aliases of D (i.e. they are other ways to refer to D).

When Mercury was first implemented in the mid-1990s, we had a student working on alias tracking. Unfortunately, what he found was that while alias tracking is possible, it was not feasible, in that it switching on alias tracking usually at least doubled the time required to compile a module. We considered this to be too high a price to pay for a capability that was just about never used. And even though today, due to Moore's law, the absolute cost of alias tracking would be much smaller, the relative tradeoffs haven't really changed, and we now have a couple of decades experience in working with Mercury in which we have found so few situations in which support for filling in partially instantiated data structures would be useful that off the top of my head I can't remember any of them.

Programming in Mercury is quite different from programming in Prolog. This is by design. In Mercury, instead of building a partially instantiated term and then filling it in, you would simply construct the final term directly. For any programmer interested in program reliability, this would be the preferred course of action even when working in Prolog. In real Prolog programs, as opposed to puzzle solvers or student exercises, leaving part of a term uninstantiated is far more likely to be an error than not.