[Haskell-cafe] slow type level function

Baojun Wang wangbj at gmail.com
Mon Apr 17 20:34:53 UTC 2017

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)

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

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

More information about the Haskell-Cafe mailing list