Coroutining in Prolog: when argument is a list (it has fixed length)

Question

Question

Is it possible to schedule a goal to be executed as soon as the length of a list is known / fixed or, as @false pointed out in the comments, a given argument becomes a [proper] list? Something along this line:

when(fixed_length(L), ... some goal ...).

When-conditions can be constructed using ?=/2, nonvar/1, ground/1, ,/2, and ;/2 only and it seems they are not very useful when looking at the whole list.

As a further detail, I'm looking for a solution that presents logical-purity if that is possible.

Motivation

I think this condition might be useful when one wants to use a predicate p(L) to check a property for a list L, but without using it in a generative way.

E.g. it might be the case that [for efficiency or termination reasons] one prefers to execute the following conjunction p1(L), p2(L) in this order if L has a fixed length (i.e. L is a list), and in reversed order p2(L), p1(L) otherwise (if L is a partial list).

This might be achieved like this:

when(fixed_length(L), p1(L)), p2(L).

Update

I did implement a solution, but it lacks purity.

Answer 1

It would be nice if when/2 would support a condition list/1. In the meantime, consider:

list_ltruth(L, Bool) :-
   freeze(L, nvlist_ltruth(L, Bool)).

nvlist_ltruth(Xs0, Bool) :-
   (  Xs0 == [] -> Bool = true
   ;  Xs0 = [_|Xs1] -> freeze(Xs1, nvist_ltruth(Xs1, Bool))
   ;  Bool = false
   ).

when_list(L, Goal_0) :-
   nvlist_ltruth(L, Bool),
   when(nonvar(Bool),( Bool == true, Goal_0 )).

So you can combine this also with other conditions.

Maybe produce a type error, if L is not a list.

   when(nonvar(Bool), ( Bool == true -> Goal_0 ; sort([], L) ).

Above trick will only work in an ISO conforming Prolog system like SICStus or GNU that produces a type_error(list,[a|nonlist]) for sort([],[a|nonlist]), otherwise replace it by:

   when(nonvar(Bool),
      ( Bool == true -> Goal_0 ; throw(error(type_error(list,L), _)).

Many systems contain some implementation specific built-in like '$skip_list' to traverse lists rapidly, you might want to use it here.

Answer 2

I've managed to answer my own question, but not with a pure solution.

Some observations

The difficulty encountered in writing a program that schedules some goal for execution when the length of a list is precisely known is the fact that the actual condition might change. Consider this:

when(fixed_length(L), Goal)

The length of the list might change if L is unbound or if the last tail is unbound. Say we have this argument L = [_,_|Tail]. L has a fixed width only if Tail has a fixed width (in other words, L is a list if T is a list). So, a condition that checks Tail might be the only thing to do at first. But if Tail becomes [a|Tail2] a new when-condition that tests if Tail2 is a list is needed.

The solution

1. Getting the when-condition

I've implemented a predicate that relates a partial list with the when-condition that signals when it might become a list (i.e. nonvar(T) where T is the deepest tail).

condition_fixed_length(List, Cond):-
    \+ (List = []),
    \+ \+ (List = [_|_]),
    List = [_|Tail],
    condition_fixed_length(Tail, Cond).
condition_fixed_length(List, Cond):-
    \+ \+ (List = []),
    \+ \+ (List = [_|_]),
    Cond = nonvar(List).

2. Recursively when-conditioning

check_on_fixed_length(List, Goal):-
    (
         condition_fixed_length(List, Condition)
     ->
         when(Condition, check_on_fixed_length(List, Goal))
     ;
         call(Goal)
    ).

Example queries

Suppose we want to check that all elements of L are a when the size of L is fixed:

?- check_on_fixed_length(L, maplist(=(a), L)).
when(nonvar(L), check_on_fixed_length(L, maplist(=(a), L))).

... and then L = [_,_|Tail]:

?- check_on_fixed_length(L, maplist(=(a), L)), L = [_,_|L1].
L = [_G2887, _G2890|L1],
when(nonvar(L1), check_on_fixed_length([_G2887, _G2890|L1], maplist(=(a), [_G2887, _G2890|L1]))).

?- check_on_fixed_length(L, maplist(=(a), L)), L = [_,_|L1], length(L1, 3).
L = [a, a, a, a, a],
L1 = [a, a, a].

Impurity

conditon_fixed_length/2 is the source of impurity as it can be seen from the following query:

?- L = [X, Y|Tail], condition_fixed_length(L, Cond), L = [a,a].
L = [a, a],
X = Y, Y = a,
Tail = [],
Cond = nonvar([]).

?- L = [X, Y|Tail], L = [a, a], condition_fixed_length(L, Cond).
false.