[Haskell-cafe] slow type level function

[Will Yager]

As I recall from the Idris paper, the compiler has special knowledge about types like Nat. As you have noticed, actually computing peano numbers is quite slow. Take a look at https://hackage.haskell.org/package/ghc-typelits-natnormalise for an example of "cheating" and embedding integers at the type level with special support. 

Will 

> On Apr 17, 2017, at 3:34 PM, Baojun Wang <wangbj at gmail.com> wrote:
> 
> 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
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20170417/2ccc85ea/attachment.html>