= Solution
The constructors `ZigType` and `ZagType` record which of the two alternating positions contains the last element. The tail types swap the two <type parameters>, so the return type of `lastZag` swaps them back:
``
lastZig :: Zig a b -> ZigOrZagType a b
lastZig Nil = error "lastZig: empty input"
lastZig (Cins x Nal) = ZigType x
lastZig (Cins _ zs) = lastZag zs
lastZag :: Zag a b -> ZigOrZagType b a
lastZag Nal = error "lastZag: empty input"
lastZag (Cans x Nil) = ZagType x
lastZag (Cans _ zs) = lastZig zs
``
For example, `lastZig` passes a tail of type `Zag b a` to `lastZag`, whose result then has type `ZigOrZagType a b`, exactly as required. Conversely, `lastZag` passes a `Zig b a` tail to `lastZig`. A singleton returns its element in the appropriate constructor; a longer input discards one element and uses <mutual recursion> on the shorter tail. This proves correctness by <structural induction> on the finite alternating sequence. The three source examples give \b[`ZigType 2`, `ZagType "D"`, and `ZigType True`].
Back to article page
