[Haskell-cafe] slow type level function

[Baojun Wang]

Thanks for the link, it seems a lot more complicated than I thought, but
understandable since the Peano arithmetic is fully recursive, it may has
the same performance issue even at value level.

This make type level Nat less attractive, I think. With TypeLits (assuming
it doesn't have the slow performance issue) it is impossible to write
something like:

add :: a -> b -> a+b
add a b = a+b

?

Thanks
Baojun
On Mon, Apr 17, 2017 at 13:48 Will Yager <will.yager at gmail.com> wrote:

> 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/20170418/4aac86c3/attachment.html>