I have couple doubts about the way dicts work in SWI:
Can Dicts be represented as semantically equivalent first-order logic program terms? I have seen in the documentation and in the C source that they are represented as terms of uneven arity, but calls to functor/3 and =…/2 seem to generate weird functors (namely “C’dict’” which in theory isn’t an allowable functor in Prolog).
Does this “C’dict’” denote an opaque C-level implementation that has no FOL equivalent and is best left alone?
How does this bode for reasoning declaratively about logic programs utilising these structures?
A dict is a compound that uses a unique atom that has no readable syntax C'dict as functor name. The arguments are first that tag and than a list of <value><key> pairs, where the keys are ordered according to the internal handle values. The C'dict thing follows from SWI-Prolog’s abstraction of atoms called blobs. Normal atoms are a subtype thereof. Other members of this family are foreign handles as are returned by open/3. Most of these can be written, but cannot be read. The empty list ([]) is also member of this family, but it can be read.
As dicts are no more than syntactic sugar for these compounds they do not introduce anything new to Prolog’s semantics. Code that merely analyses Prolog data works the same except that it must realize that functor names may not be atoms (but are atomic). Code that rewrites Prolog data must respect the additional constraints of a dict compared to a normal compound. Most of that code gets clearer by introducing a clause that handles dicts before compounds.
Note that future versions may change the internals.
As for reasoning about program-as-data, dicts are not of the type callable and thus cannot be used to create a clause head.