Test that term is a list of distinct variables

Question

What is the most compact and canonical way in ISO Prolog to test for a list of distinct variables? Let's call this meta-logical predicate is_varset/1.

So it should succeed if its argument is a list of variables that are all different. Note that a list always contains a [] at its end. If a variable is at the end, we call this a partial list (which is thus not a list). And if a non-variable term occurs as a suffix that is neither [] nor a variable, then this is neither a partial list nor a list.

A notable special case of a term being neither a partial list nor a list are infinite lists. They contain at least two suffixes that are identical, actually they then possess infinitely such suffixes. Infinite lists are out of scope of the standard — all attempts to create them result in a STO unification whose result is undefined. Still, some systems support them, so ideally for those infinite lists, is_varset/1 should fail finitely.

?- is_varset([A|nonlist]).
false.

?- is_varset([A,B]), is_varset([B,A]).
true.

?- is_varset([A,B,A]).
false.

?- is_varset([A,f(B)]).
false.

?- is_varset([A|_]).
false.

?- L = [_|L], is_varset(L).  % may loop, should rather terminate
false.

Here is an overview of the built-ins in ISO/IEC 13211-1:1995 including Cor.2:2012.

Answer 1

this simple definition in SWI-Prolog seems to accomplish the requirements

is_varset(Vs) :- /*is_list(Vs),*/ term_variables(Vs, T), T == Vs.