<div dir="ltr">Hello cafe,<div><br></div><div>I tried to play with some type level natural numbers, and it seems type level function is quite slow, for instance:</div><div><br></div><div>(full source)</div><div><a href="https://gist.github.com/wangbj/5939aa7a30c3d756d98f5b5775e162a6">https://gist.github.com/wangbj/5939aa7a30c3d756d98f5b5775e162a6</a><br></div><div><br></div><div><div><font face="monospace">data Z</font></div><div><font face="monospace">data S n</font></div><div><font face="monospace"><br></font></div><div><font face="monospace">class KnownNat n where</font></div><div><font face="monospace">  natSing :: n -> Integer</font></div><div><font face="monospace"><br></font></div><div><font face="monospace">instance KnownNat Z where</font></div><div><font face="monospace">  natSing _ = 0</font></div><div><font face="monospace">instance KnownNat n => KnownNat (S n) where</font></div><div><font face="monospace">  natSing _ = 1 + natSing (undefined :: n)</font></div><div><font face="monospace"><br></font></div><div><font face="monospace">natVal :: KnownNat n => n -> Integer</font></div><div><font face="monospace">natVal = natSing</font></div></div><div><br></div><div>natSing doesn't seems to know how to optimize when KnownNat is very big (i.e: 10000), I tried Peano Add/Mul, and they are very slow to be really useful. Is there any ways to improve this? How fully dependent typed language such as Adga/Idris handle this, do they have the same performance issue?</div><div><br></div><div>Thanks</div><div>baojun</div></div>