From a83cef83608ba7f2dd603e968d36464363a1752d Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Tue, 14 Jan 2025 16:02:39 -0500
Subject: [PATCH] Add choose utilties to util

---
 src/Util/Eff.md | 25 +++++++++++++++++++++++++
 1 file changed, 25 insertions(+)

diff --git a/src/Util/Eff.md b/src/Util/Eff.md
index 6025de3..40517ea 100644
--- a/src/Util/Eff.md
+++ b/src/Util/Eff.md
@@ -155,3 +155,28 @@ export
 trace : Has Logger fs => Lazy String -> Eff fs ()
 trace x = send $ Log Trace x
 ```
+
+## Choose
+
+Lifts any foldable data structure into the Choose effect, enabling the style of
+nondeterministic programming from the list monad
+
+```idris
+export
+oneOf : Has (Choose) fs => Foldable f =>
+    f a -> Eff fs a
+oneOf x = foldl oneOf' empty x
+  where
+  oneOf' : Eff fs a -> a -> Eff fs a
+  oneOf' acc val = pure val `alt` acc
+```
+
+Lifts any foldable of effectful computations into the Choose effect much the
+same as `oneOf`
+
+```idris
+export
+oneOfM : Has (Choose) fs => Foldable f =>
+    f (Eff fs a) -> Eff fs a
+oneOfM x = foldl alt empty x
+```