Printing cyclic terms

I’d like to suggest a new way for printing cyclic terms. Some systems (e.g. SICStus, SWI), support representing cyclic terms in output as follows

?- X=f(Y), Y=g(Y), write_term(X,[]).
@(f(_123),[_123=g(_123)])

Here, the cyclic subterms are factored out using introduced variables, and all references to the cyclic terms replaced with the corresponding variable. The whole output consists of a term of the form

@(SimplifiedTerm, DefinitionsOfCyclicSubterms)

It is a somewhat ad hoc solution that I was not comfortable with, for reasons such as

  • the need for a reserved functor @/2
  • the use of a top-level wrapper instead of something local to the cyclic subterm
  • non-compositionality of such wrapped terms

I would therefore like to propose an alternative notation based on attributed variables and the apparently growing consensus around a Var{AttrName:AttrValue} notation.

The main idea is simply that a variable’s value can be considered one of its attributes. If we call this (pseudo-)attribute value, the cyclic term above can be written as

f(_123{value:g(_123)})

As above, in effect the cyclic term is replaced by an introduced variable. The first occurrence of the cyclic term is printed as this variable, annotated with a value-attribute. This (pseudo-)attribute is the cyclic term itself, but with all cyclic references replaced by the plain new variable (without attribute annotation).
This abuse of the already familiar syntax for variable attributes permits to effectively label subterms (with pseudo-variable names), and refer to these labels, in order to denote cycles.
Since cycle detection can be expensive, I would suggest to enable this feature only via an option to write_term/2,3.
Note that the idea has interesting further potential such as

  • possible support in the parser
  • generalisation beyond cycles, to any shared subterms