[Haskell-cafe] slow type level function
will.yager at gmail.com
Mon Apr 17 20:48:01 UTC 2017
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.
> 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)
> 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?
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> Only members subscribed via the mailman list are allowed to post.
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Haskell-Cafe