Singleton variables warning in branches, in the type_check library

Help!
1

I recently cloned Tom Schrijvers’ type_check library to understand it better and hopefully make a small number of improvements/documentation and make it available again as a pack.

When importing that library, a singleton variable warning is generated for lines like:

:- type list(T)     ---> [] ; [T|list(T)].

(that’s defined in the library itself, see here).

Oddly, this other version, that doesn’t have branches, would work without warnings:

:- type list(T)     ---> [T|list(T)].

So I guess the error is saying that if we assigned a procedural meaning to that code and choose the [] branch, I would have list[T] ---> [] and that T is a singleton variable. This is a substantial problem because it will generate a warning also for each user-defined polymorphic type that doesn’t have all the type variables in each constructor.

My question for you is: what could I do to convince swipl that that warning is undeserved? I know that I could disable singletons checking via :- style_check(-singleton). but that seems a very heavy hammer: I actually want singleton checking, it’s just that it shouldn’t happen here.

2

I thought the solution could have been be not using ;/2 that seems to have a special meaning, and using a newly defined |/2 instead, so that the body of the type declaration is seen as just a term;

It seems that was insufficient, since I still get the error with a sum datatype, even if I write it with |/2.
Any advice?

3

To find out, we run the code below. The T='$VAR'('T') is a very dirty trick to get the variable names into the output of portray_clause/1. Only use as a hack on the toplevel!

We see that in the first clause the variable T appears as singleton in both branches. Haven’t studied this, but this seems a bit worrying to me. If the generated code is really correct the generator should replace the T with a fresh variable. If that is too complex, the clause generator could at the end perform a copy_term/2. Then there is still a sharing variable, but as it is not related to a variable in the source, the compiler doesn’t report it.

?- expand_term((:- type list(T) ---> [] ; [T|list(T)]), Clauses),
    T='$VAR'('T'),
    maplist(portray_clause, Clauses).

type_check:constructor([], B, A, A) :-
    (   type_check:equate_types(B, list(T))
    ->  true
    ;   type_check:term_type_error([], B, list(T))
    ),
    true.
type_check:constructor_info([], list(T), [], []).
type_check:constructor([B|C], A, D, F) :-
    (   type_check:equate_types(A, list(T))
    ->  true
    ;   type_check:term_type_error([B|C], A, list(T))
    ),
    type_check:type_check_term(B, T, D, E),
    type_check:type_check_term(C, list(T), E, F),
    true.
type_check:constructor_info([A|B], list(T), [A, B], [T, list(T)]).
1 Like
4

Thanks for the answer @jan! The T='$VAR'('T') trick is very nice! I wonder though, what are the ways in which $VAR/1 is special? Only in the fact that is printed as the corresponding variable? I see that’s also the result of the numbervars predicate.

Reading your insight, I can see that freshening the variables before we start the computation for the clauses allows us to decouple the variables in the source code from the one in the generated clauses.
This brought to this commit that solves neatly the problem.

Thanks again :slight_smile:

1 Like
5

It is (as you note) used by numbervars/3. write_term/2 and friends print ‘$VAR’(N) as 1->A, 2->B, etc.
SWI-Prolog extended this to print ‘$VAR’(Atom) as Atom, provided Atom satisfies the syntax of a Prolog variable. In the recent versions portray_clause/3 also accepts a variable_names(List) option.

2 Likes