  We introduce a novel framework, termed $\lambda$DD, that revisits Binary
Decision Diagrams from a purely functional point of view. The framework allows
to classify the already existing variants, including the most recent ones like
Chain-DD and ESRBDD, as implementations of a special class of ordered models.
We enumerate, in a principled way, all the models of this class and isolate its
most expressive model. This new model, termed $\lambda$DD-O-NUCX, is suitable
for both dense and sparse Boolean functions, and is moreover invariant by
negation. The canonicity of $\lambda$DD-O-NUCX is formally verified using the
Coq proof assistant. We furthermore give bounds on the size of the different
diagrams: the potential gain achieved by more expressive models can be at most
linear in the number of variables n.
