idris-lang
Incorrect running times for Data.Seq due to missing laziness
It seems that the Finger-tree implementation in Data.Seq.Internal has a strict spine (since idris is strict by default). However, in order to guarantee that operations such as cons, snoc, viewl, and viewr actually achieve O(1) running time (as claimed in the modules that use this module (e.g. Data.Seq.Sized and Data.Seq.Unsided) the spine needs to be lazy. See page 203 of the Hinze & Paterson paper that introduced Finger trees.
Any updates on this? Just curious if this is truly an issue based on the way Sequences are implemented in Haskell.
Any updates on this?
I don't think anything has happened since.
Just curious if this is truly an issue based on the way Sequences are implemented in Haskell.
I'm not sure what exactly you mean by this? Just to be clear: the Data.Sequence implementation in the containers library in Haskell is perfectly fine (as the spine is lazy). However, since the spine needs to be lazy, the idris version is not.
Any updates on this?
I don't think anything has happened since.
Just curious if this is truly an issue based on the way Sequences are implemented in Haskell.
I'm not sure what exactly you mean by this? Just to be clear: the Data.Sequence implementation in the containers library in Haskell is perfectly fine (as the spine is lazy). However, since the spine needs to be lazy, the idris version is not.
Ah okay, yeah this is what I was trying to get at, thank you!
Any updates on this? Just curious if this is truly an issue based on the way Sequences are implemented in Haskell.
A year ago I made an alternative Idris implementation with an explicitly lazy spine, but didn't find any program that could show the difference in the performance (but maybe I was not good enough in this, because I didn't use any automated techniques, but I should have to do)
A year ago I made an alternative Idris implementation with an explicitly lazy spine, but didn't find any program that could show the difference in the performance (but maybe I was not good enough in this, because I didn't use any automated techniques, but I should have to do)
Oh, that is very interesting! I would have assumed that not having an explicitly lazy spine would affect things performance-wise.
Any updates on this? Just curious if this is truly an issue based on the way Sequences are implemented in Haskell.
A year ago I made an alternative Idris implementation with an explicitly lazy spine, but didn't find any program that could show the difference in the performance (but maybe I was not good enough in this, because I didn't use any automated techniques, but I should have to do)
How was the performance for concatenation, splitting, access, etc. vs a list?