This is cute notation-wise, but certainly not "best practices", given that the more idiomatic knot-tying version uses O(1) memory, and this uses O(n).

Empty strings naturally has a score of 0.

There are no words in an empty string, and so no maximum word. An empty string is really not the expected answer, as the empty string is not a word in the empty string.

Reading the test code, I think I see the problem. It is testing the absolute error, i.e. abs(x-y) < 1.e-12. That is a mistake; if x and y are both small then this will be true even if they are quite different. For example: by this test 1.000000000000000e-12 ~ 1.999999999999999e-12, even though one is almost twice as big as the other. You should really be testing the relative error in stead, i.e. abs((x-y)/(x+y)) < 5.e-13. In other words, right now it is checking if x and y agree to the 12th digit after the decimal point, but it should be checking that they agree to 12 significant digits. In the case of Forth, it's a simple matter of changing f~abs to f~rel.

Right, I was thinking laziness would save us from fully evaluating init O(n) times, but on second thought it doesn't.

The type signature +-pzero : ∀ n {p} → n p+ pzero ≡ n is a little weird, shouldn't it be +-pzero : ∀ n → n p+ pzero ≡ n?

Very cute! Am I right that this will be inefficient, though, as it builds up a tower of thunks?