We study issues that arise in programming with primitive recursion
over non-free datatypes such as lists, bags and sets. Programs written
in this style can lack a meaning in the sense that their outputs may
be sensitive to the choice of input expression. We are, thus,
naturally lead to a set-theoretic denotational semantics with partial
functions. We set up a logic for reasoning about the definedness of
terms and a deterministic and terminating evaluator. The logic is
shown to be sound in the model, and its recursion free fragment is
shown to be complete for proving definedness of recursion free
programs. The logic is then shown to be as strong as the evaluator,
and this implies that the evaluator is compatible with the provable
equivalence between different set (or bag, or list)
expressions. Oftentimes, the same non-free datatype may have different
presentations, and it is not clear a priori whether programming and
reasoning with the two presentations are equivalent. We formulate
these questions, precisely, in the context of alternative
presentations of the list, bag, and set datatypes and study some
aspects of these questions. In particular, we establish back-and-forth
translations between the two presentations, from which it follows that
they are equally expressive, and prove results relating proofs of
program properties, in the two presentations.