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 issue?
Thanks
baojun