reduce<D>

Let's first consider specializing reduce to a simple type, like D or C. In this case, then reduce will have the following type:
reduce<D> :: $\gamma$ $\rightarrow$($\gamma$ $\rightarrow$$\gamma$ $\rightarrow$$\gamma$) $\rightarrow$(D $\rightarrow$$\gamma$)

In order to specialize, we need a way of relating the datatype D to the mini constructor language. To this end, we introduce a new datatype D$^\circ$ that is isomorphic to D, but only uses the constructors of the mini constructor language: data D$^\circ$ = 1 :+: (1 :+: ( $\ldots$ )) We further introduce two functions that witness the isomorphism: fromD :: D $\rightarrow$D$^\circ$
fromD Sun = Inl Unit
fromD Mon = Inr (Inl Unit)
$\ldots$
toD :: D$^\circ$ $\rightarrow$D
fromD (Inl Unit) = Sun
fromD (Inr (Inl Unit)) = Mon
$\ldots$

We specialize reduce to D$^\circ$ by simply unrolling the definition: D$^\circ$:
reduce<D$^\circ$> $c$ $\oplus$ = red<D$^\circ$>
where
red<D$^\circ$>
= red<1 :+: (1 :+: ( $\ldots$) )>
= red<:+:> red<1> (red<1 :+: ( $\ldots$ )>)
= red<:+:> red<1> (red<:+:> red<1> ( $\ldots$ )) Now, we have implementations of red<:+:> and red<1> given in the definition of reduce, which can be used here to complete the definition of reduce<D$^\circ$>.

How do we specialize reduce to D? The simplest way is to use reduce<D$^\circ$> along with the function fromD:
reduce<D> $c$ $\oplus$ = (reduce<D$^\circ$> $c$ $\oplus$) $\circ$ fromD

We might well wonder ``What is the use of reduce<D>?'' It is not hard to see that reduce<D> $c$ $\oplus$ $v$ returns $c$ for all values $v$ of type D. We might think then that reduce is not a useful function, but the usefulness of reduce becomes apparent when it is specialized to type constructors like L and B.