Open hellwolf opened 1 year ago
Graham Hutton has an excellent advanced functional programming in Haskell which also discussed the faster reverse: https://www.youtube.com/watch?v=WQy7Bzr03R4
It would be a good exercise to do an Agda proof of it.
reverse' :: [a] -> [a] -> [a] reverse' [] ys = ys reverse' (x:xs) ys = reverse' xs (x: ys) -- | Faster reverse in O(n). reverse :: [a] -> [a] reverse xs = reverse' xs []
Yeah, this is basically analogous to implementing it using foldl. It's also a good exercise to prove that this reverse and the one in the presentation are equivalent.
foldl
Graham Hutton has an excellent advanced functional programming in Haskell which also discussed the faster reverse: https://www.youtube.com/watch?v=WQy7Bzr03R4
It would be a good exercise to do an Agda proof of it.