  Nested relations, built up from atomic types via product and set types, form
a rich data model. Over the last decades the nested relational calculus, NRC,
has emerged as a standard language for defining transformations on nested
collections. NRC is a strongly-typed functional language which allows building
up transformations using tupling and projections, a singleton-former, and a map
operation that lifts transformations on tuples to transformations on sets.
  In this work we describe an alternative declarative method of describing
transformations in logic. A formula with distinguished inputs and outputs gives
an implicit definition if one can prove that for each input there is only one
output that satisfies it. Our main result shows that one can synthesize
transformations from proofs that a formula provides an implicit definition,
where the proof is in an intuitionistic calculus that captures a natural style
of reasoning about nested collections. Our polynomial time synthesis procedure
is based on an analog of Craig's interpolation lemma, starting with a provable
containment between terms representing nested collections and generating an NRC
expression that interpolates between them.
  We further show that NRC expressions that implement an implicit definition
can be found when there is a classical proof of functionality, not just when
there is an intuitionistic one. That is, whenever a formula implicitly defines
a transformation, there is an NRC expression that implements it.
