reduce<L> and reduce<B>

Without justification, we assert that the type of reduce<L> is the following:
reduce<L> :: $\gamma$ $\rightarrow$($\gamma$ $\rightarrow$$\gamma$ $\rightarrow$$\gamma$) $\rightarrow$( $\forall \alpha$. ($\alpha$ $\rightarrow$$\gamma$) $\rightarrow$L $\alpha$ $\rightarrow$$\gamma$)

As with reduce<D>, we introduce a new datatype isomorphic to L:
data L$^\circ$ $\alpha$ = 1 :+: ($\alpha$ :*: (L $\alpha$))
fromL :: L $\rightarrow$L$^\circ$
fromL Nil = Inl Unit
fromL (Cons x xl) = Inr (x :*: xl)
toL :: L$^\circ$ $\rightarrow$L
toL (Inl Unit) = Nil
toL (Inr (x :*: xl)) = Cons x xl
Note that L$^\circ$ is defined in terms of L. L$^\circ$ is isomorphic to ``one unrolling'' of L, which is sufficient for our purposes.

We proceed with specialization of reduce to L$^\circ$ by unrolling the definition. The ``new'' argument in the type of reduce<L> above corresponds to ``what to do'' when the unrolling encounters the polymorphic type variable $\alpha$: reduce<L> $c$ $\oplus$ ra = (reduce<L$^\circ$> $c$ $\oplus$ ra) $\circ$ fromL
reduce<L$^\circ$> $c$ $\oplus$ ra = red<L$^\circ$>
where
red<L$^\circ$>
= red<1 :+: ($\alpha$ :*: (L $\alpha$))>
= red<:+:> red<1> red<$\alpha$ :*: (L $\alpha$)>
= red<:+:> red<1> (red<:*:> red<$\alpha$> red<L $\alpha$>)
At this point, we can use ra as the interpretation of red<$\alpha$>
= red<:+:> red<1> (red<:*:> ra red<L $\alpha$>)
Furthermore, we interpret the type application in L $\alpha$ as the value application red<L> red<$\alpha$>
= red<:+:> red<1> (red<:*:> ra (red<L> red<$\alpha$>))
= red<:+:> red<1> (red<:*:> ra (red<L> ra>))
For reasons that aren't entirely apparent from the ad hoc approach we've taken to defining polytypic functions and to specializing polytypic functions, the appropriate interpretation of red<L> is reduce<L> $c$ $\oplus$>. Hopefully, this at least makes intuitive sense.
= red<:+:> red<1> (red<:*:> ra ((reduce<L> $c$ $\oplus$) ra>))

Similarly, we attack the specialization of reduce to B:
reduce<B> :: $\gamma$ $\rightarrow$($\gamma$ $\rightarrow$$\gamma$ $\rightarrow$$\gamma$) $\rightarrow$( $\forall \alpha$. ($\alpha$ $\rightarrow$$\gamma$) $\rightarrow$B $\alpha$ $\rightarrow$$\gamma$)

data B$^\circ$ $\alpha$ = 1 :+: ($\alpha$ :*: (B (B $\alpha$)))
fromB :: B $\rightarrow$B$^\circ$
fromB NilB = Inl Unit
fromB (ConsB x xb) = Inr (x :*: xb)
toB :: B$^\circ$ $\rightarrow$B
toB (Inl Unit) = NilB
toB (Inr (x :*: xb)) = ConsB x xb

reduce<B> $c$ $\oplus$ ra = (reduce<B$^\circ$> $c$ $\oplus$ ra) $\circ$ fromB
reduce<B$^\circ$> $c$ $\oplus$ ra = red<B$^\circ$>
where
red<B$^\circ$>
= red<1 :+: ($\alpha$ :*: (B (B $\alpha$)))>
= red<:+:> red<1> red<$\alpha$ :*: (B (B $\alpha$))>
= red<:+:> red<1> (red<:*:> red<$\alpha$> red<B (B $\alpha$)>)
= red<:+:> red<1> (red<:*:> red<$\alpha$> (red<B> red<B $\alpha$>))
= red<:+:> red<1> (red<:*:> red<$\alpha$> (red<B> (red<B> red<$\alpha$>)))
= red<:+:> red<1> (red<:*:> ra (red<B> (red<B> ra)))
= red<:+:> red<1> (red<:*:> ra ((reduce<B> $c$ $\oplus$) ((reduce<B> $c$ $\oplus$) ra)))

Finally, consider the following instantiations of reduce:

fsize<$\mathcal{F}$> :: $\mathcal{F}$ $\alpha$ $\rightarrow$Int
fsize<$\mathcal{F}$> = reduce<$\mathcal{F}$> 0 (+) (const 1)

fall<$\mathcal{F}$> :: ($\alpha$ $\rightarrow$Bool) $\rightarrow$$\mathcal{F}$ $\alpha$ $\rightarrow$Bool
fall<$\mathcal{F}$> p = reduce<$\mathcal{F}$> True ($\wedge$) p

fflatten<$\mathcal{F}$> :: $\mathcal{F}$ $\alpha$ $\rightarrow$L $\alpha$
fflatten<$\mathcal{F}$> = reduce<$\mathcal{F}$> Nil (++) wrap
where wrap x = Cons x Nil