[ add ] Natural number square root

[jamesmckinna]

Fixes #2231 for Nat.

[gallais]

Does it really need to be in its own module as opposed to just being in Data.Nat.Base?

[jamesmckinna]

Does it really need to be in its own module as opposed to just being in Data.Nat.Base?

No, surely not. But like Logarithm, (and with @JacquesCarette 's pleas for small modules in my head...) I was starting to wonder if the transcendental/irrational functions deserved more/separate space for their definition and properties. But since this is currently entirely self-contained, for sure it can move to Data.Nat.Base, and can be refactored accordingly.

I think this perhaps should be marked DRAFT until all of the above shakes out? I just needed to get it out of my head...

[JacquesCarette]

As Data.Nat.Base already depends on Data.Bool.Base, I don't object to moving it there. I prefer the way it is now.

[JacquesCarette]

My suggestion is not a deal-breaker.

[JacquesCarette]

Maybe 2*_ should be a function in Data.Nat.Base that is exported?

[gallais]

Note that the generated code will be slower than simply using 2 * m.

[jamesmckinna]

Thanks for all the commentary. I suppose I'd opted for Goodstein out of a failure to write a 'nice' odd/even mutual recursion by wf-induction which starts with n / 2 and appropriately Newton-Raphson iterates to convergence. But like much at the moment, inspired design thoughts are just as likely as plodding test case failure bewilderment. Sigh.

[gallais]

write a 'nice' odd/even mutual recursion by wf-induction

Have you considered doing an induction of the Data.Nat.Binary representation
of the natural number?

[jamesmckinna]

write a 'nice' odd/even mutual recursion by wf-induction

Have you considered doing an induction of the Data.Nat.Binary representation of the natural number?

Well, wouldn't that be a thing to try!? But no, until you suggested it, no, I hadn't. A case of too-narrowly-bounded brainwidth!

[Taneb]

I think you're aware of the issues here, but I don't think we should merge this as-is. The current definition is neither (to me) obviously correct, nor is it fast (I'm actually surprised with how slow it is! something seems wrong there). I had a little go doing something Newton-y, but it's tricky

[jamesmckinna]

Thanks @Taneb . Two things:

• I agree with you, and woke up thinking I should convert to DRAFT, which I will do
• Please feel free to exercise your veto power on merging by posting a Request Changes review... it's sometime burdensome to relitigate/unpick such a thing, but in this case, fair comment!

Oh, and a third: I'm sure the definitions are "obviously correct", but YMMV ;-) and irrational convictions on the part of authors, human and/or otherwise, are part of what our processes are designed to catch!