[1..1000] takes a long time.

[kmarekspartz]

It looks like using Nats in enumFromTo is slowing things down. Is there a way to speed this up without losing simplicity and reasonability?

[david-christiansen]

It's possible that they are slowing things down. The present implementation
was written with an eye towards making the syntax work in proofs, so it
uses Nats in order to make it obviously total.

Why on earth would you want to write [1..1000] in a strict language though?
This strikes me as a somewhat unimportant use case, but I could be missing
something obvious.

[LeifW]

And, to be clear: are you talking about the REPL or compiled code here? The repl takes many orders of magnitude longer on stuff like this.

[kmarekspartz]

Sorry, I was trying out the REPL.

Here's my use case:

sum $ map (\x => x * x) [1..1000]

It shouldn't matter whether it is lazy or strict, as other languages, both lazy and strict handle it fine.

I do understand that it presently makes the proofs work well, and that optimization comes later.

[david-christiansen]

@raichoo just rewrote this to be tail-recursive - it still goes slowly for me, so I imagine that tail recursion isn't a big win in the REPL evaluator.

I'm wondering if this is reasonably solvable in a way other than documentation...

[jfdm]

This looks like it is related to Issue #172

[ahmadsalim]

I think this is a duplicate of #172 as @jfdm mentioned, so I will close this.