Polytypic reduce

The reduction of a datatype replaces elements of a base type with a constant and replaces the pair constructor with a binary operation. It is very similar to the function foldr on a list.

Our goal is to write a single version of reduce that can (automatically) be specialized to any datatype. However, as noted earlier, datatypes encompass a large number of features. To make writing polytypic functions feasible, we write them in terms of a minimalistic constructor language. This mini constructor language has ``terms'' for primitive types (Int, Float, etc.), the unit type (data 1 = Unit), binary sums (data $\alpha$ :+: $\beta$ = Inl $\alpha$ | Inr $\beta$), and binary products (data $\alpha$ :*: $\beta$ = ($\alpha$, $\beta$)). To define a polytypic function, it suffices to define the action of the function at these terms.

Without further ado, here is the polytypic version of reduce: reduce<t> $c$ $\oplus$ = red<t>
where
red<1> Unit = $c$
red<Int> i = $c$
red<Float> f = $c$
red<:+:> reda redb (Inl x) = reda x
red<:+:> reda redb (Inr y) = redb y
red<:*:> reda redb (x, y) = $\oplus$ (reda x) (redb y)