[Haskell-cafe] slow type level function

[Baojun Wang]

Hello cafe,

I tried to play with some type level natural numbers, and it seems type
level function is quite slow, for instance:

(full source)
https://gist.github.com/wangbj/5939aa7a30c3d756d98f5b5775e162a6

data Z
data S n

class KnownNat n where
  natSing :: n -> Integer

instance KnownNat Z where
  natSing _ = 0
instance KnownNat n => KnownNat (S n) where
  natSing _ = 1 + natSing (undefined :: n)

natVal :: KnownNat n => n -> Integer
natVal = natSing

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?

Thanks
baojun
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20170417/9c2bcdbe/attachment.html>