  In dependently typed programming, proofs of basic, structural properties can
be embedded implicitly into programs and do not need to be written explicitly.
Besides saving the effort of writing separate proofs, a most distinguishing and
fascinating aspect of dependently typed programming is that it makes the idea
of interactive type-driven development much more powerful, where expressive
type information becomes useful hints that help the programmer to complete a
program. There have not been many attempts at exploiting the full potential of
the idea, though. As a departure from the usual properties dealt with in
dependently typed programming, and as a demonstration that the idea of
interactive type-driven development has more potential to be discovered, we
conduct an experiment in ?type-driven algorithm design?: we develop algorithms
from their specifications encoded in sophisticated types, to see how useful the
hints provided by a type-aware interactive development environment can be. The
algorithmic problem we choose is metamorphisms, whose definitional behaviour is
consuming a data structure to compute an intermediate value and then producing
a codata structure from that value, but there are other ways to compute
metamorphisms. We develop Gibbons?s streaming algorithm and Nakano?s jigsaw
model in the interactive development environment provided by the dependently
typed language Agda, turning intuitive ideas about these algorithms into formal
conditions and programs that are correct by construction.
