Post #1782150

@screwlisp wrote: «This made me think about using pow on rational inputs. Well, rightly it says "hey I have no idea how you are planning to get a rational type out of this without you telling me something" ! Which is, I guess what one wants from a type theory.» The traditional approach is to go a few extra miles and compute exact roots of integers (and hence rationals) where they exist. Thus, for example, compute the fifth root of integer 243 as integer 3, rather than floating-point 3.0. (It's not neurosurgery, but in many cases the extra effort is difficult to justify.) I don't know whether type theory can help here. @simon_brooke