From 44245e1683c99ea1583d05e8130b8d5fd965103f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Stefan=20H=C3=B6ck?= <hock@zhaw.ch>
Date: Fri, 28 Jan 2022 10:01:09 +0100
Subject: [PATCH] [ fix ] issue #2288 (#2289)

---
 libs/prelude/Prelude/Types.idr | 12 ++++++++++--
 tests/prelude/bind001/bind.idr | 14 ++++++++++++++
 tests/prelude/bind001/expected |  4 ++++
 tests/prelude/bind001/input    |  2 ++
 tests/prelude/bind001/run      |  3 +++
 5 files changed, 33 insertions(+), 2 deletions(-)
 create mode 100644 tests/prelude/bind001/bind.idr
 create mode 100644 tests/prelude/bind001/expected
 create mode 100644 tests/prelude/bind001/input
 create mode 100755 tests/prelude/bind001/run

diff --git a/libs/prelude/Prelude/Types.idr b/libs/prelude/Prelude/Types.idr
index fb27da2a9d..513e1866b4 100644
--- a/libs/prelude/Prelude/Types.idr
+++ b/libs/prelude/Prelude/Types.idr
@@ -455,10 +455,18 @@ Foldable List where
 
   foldMap f = foldl (\acc, elem => acc <+> f elem) neutral
 
+-- tail recursive O(n) implementation of `(>>=)` for `List`
+public export
+listBind : List a -> (a -> List b) -> List b
+listBind as f = go Nil as
+  where go : List b -> List a -> List b
+        go xs []        = reverse xs
+        go xs (y :: ys) = go (reverseOnto xs (f y)) ys
+
 public export
 Applicative List where
   pure x = [x]
-  fs <*> vs = concatMap (\f => map f vs) fs
+  fs <*> vs = listBind fs (\f => map f vs)
 
 public export
 Alternative List where
@@ -467,7 +475,7 @@ Alternative List where
 
 public export
 Monad List where
-  m >>= f = concatMap f m
+  (>>=) = listBind
 
 public export
 Traversable List where
diff --git a/tests/prelude/bind001/bind.idr b/tests/prelude/bind001/bind.idr
new file mode 100644
index 0000000000..f939c42165
--- /dev/null
+++ b/tests/prelude/bind001/bind.idr
@@ -0,0 +1,14 @@
+import Data.SnocList
+
+iterateTR : Nat -> (a -> a) -> a -> List a
+iterateTR n f = go n Lin
+  where go : Nat -> SnocList a -> a -> List a
+        go 0     sx _ = sx <>> Nil
+        go (S k) sx v = go k (sx :< v) (f v)
+
+main : IO ()
+main = do
+  -- this checks that *bind* still behaves correctly
+  printLn $ [1..4] >>= (\n => iterateTR n (+1) 1)
+  -- this verifies that *bind* runs in linear time
+  printLn . length $ [1..5000] >>= (\n => iterateTR n (+1) n)
diff --git a/tests/prelude/bind001/expected b/tests/prelude/bind001/expected
new file mode 100644
index 0000000000..25d747481c
--- /dev/null
+++ b/tests/prelude/bind001/expected
@@ -0,0 +1,4 @@
+1/1: Building bind (bind.idr)
+Main> [1, 1, 2, 1, 2, 3, 1, 2, 3, 4]
+12502500
+Main> Bye for now!
diff --git a/tests/prelude/bind001/input b/tests/prelude/bind001/input
new file mode 100644
index 0000000000..fc5992c298
--- /dev/null
+++ b/tests/prelude/bind001/input
@@ -0,0 +1,2 @@
+:exec main
+:q
diff --git a/tests/prelude/bind001/run b/tests/prelude/bind001/run
new file mode 100755
index 0000000000..0df264d40a
--- /dev/null
+++ b/tests/prelude/bind001/run
@@ -0,0 +1,3 @@
+rm -rf build
+
+$1 --no-color --console-width 0 --no-banner bind.idr < input