This one is aimed at beginners learning to write their first recursive functions. It describes a technique that I found useful, back when I taught Haskell to first-year students.
http://jackkelly.name/blog/archives/2023/01/08/deriving_simple_recursive_functions/
I also teach Haskell to first-years. In our case, students are very well grounded in the notion of proof by induction (especially proofs over the naturals). This makes the introduction of simple recursion much easier by analogy to induction.
The obvious example is the factorial function:
fac 0 = 1
fac n = n * (n-1)
We can view this as a proof that $n! = Π_{1…n} n$. The first line constitutes the base case, and the second line the inductive step. The same definition of factorial is already a well-known recurrence which anyone who has taken pre-calc (or Core maths at A-level in the UK) will recognise.
The same idea can be used for product by inducting over suffixes of the input.
It’s interesting to see your alternative take, thanks for sharing!
I think of it as an alternative presentation of the same idea of induction. “Hey 2 * 3 * 4 * 5 looks like 2 * product [3, 4, 5]” is exemplifiying the induction proof underneath.
While we are at it, shameless plug of how I do it. To be fair, my students are 2nd/3rd year and have seen even “prove this inequality containing unknown constants, during the proof discover good values for the constants”, so it is a bit more believable that you can discover code during the proof too. To be fair^2, even 50yos fear recursion as much as total newbies do.
To be sure, I got from Graham Hutton, maybe also Ralf Hinze and Richard Bird etc., the idea of starting the proof first and letting the code emerge later.
On exams, I legit give hints like “Notice product [2, 3, 4, 5] = 2 * 3 * 4 * 5 = 2 * product [3, 4, 5] hint hint wink wink”, albeit for tougher questions than product.