A Formal Comparison of Approaches to Datatype-Generic Programming