Conor McBride: Seeing and Doing

• In the former approach (doing), you typically need general recursion, and termination has to be proved "after the fact".
• In the latter (seeing), structural recursion is enough! You get a termination proof for free!
• The more powerful the type system, the better your data structure can can capture the structure of the computations. Dependent types are powerful.