  It is well-known that GADTs do not admit standard map functions of the kind
supported by ADTs and nested types. In addition, standard map functions are
insufficient to distribute their data-changing argument functions over all of
the structure present in elements of deep GADTs, even just deep ADTs or nested
types. This paper develops an algorithm for detecting exactly which functions
are mappable over data whose types are (deep) GADTs. The algorithm takes as
input a term t whose type is an instance of a deep GADT D and a function f to
be mapped over t. It detects a minimal possible shape of t as an element of D,
and returns a minimal set of constraints f must satisfy to be mappable over t.
The crux of the algorithm is its ability to separate t's essential structure as
an element of D -- i.e., the part of t that is essential for it to have the
shape of an element of D -- from its incidental structure as an element of D --
i.e., the part of t that is simply data in the positions of this shape. The
algorithm ensures that the constraints on f come only from t's essential
structure. This work is part of an ongoing effort to define initial algebra
semantics for GADTs that properly generalizes the usual semantics for ADTs and
nested types as least fixpoints of higher-order endofunctors.
