Some more work on monads

1 files changed, 50 insertions, 0 deletions

diff --git a/std/Monad/List.bruijn b/std/Monad/List.bruijn
new file mode 100644
index 0000000..6c29d5a
--- /dev/null
+++ b/std/Monad/List.bruijn
@@ -0,0 +1,50 @@
+# MIT License, Copyright (c) 2023 Marvin Borner
+# monadic interface for anything based on lists (e.g. IO, strings)
+# afaik originally proposed by John Tromp and inspired by Haskell
+
+:import std/List .
+:import std/Combinator .
+
+read [0] ⧗ a → (M a)
+
+return [[1 : 0]] ⧗ a → (M a)
+
+pure return ⧗ a → (M a)
+
+# monadic bind operator
+bind [[[2 0 1]]] ⧗ (M a) → (a → (M b)) → (M a)
+
+…>>=… bind
+
+:test ((read >>= return) "woa") ("woa")
+
+# monadic reverse bind operator
+…=<<… \…>>=… ⧗ (a → (M b)) → (M a) → (M b)
+
+:test ((return =<< read) "woa") ("woa")
+
+# monadic compose operator
+…>>… [[1 >>= [1]]] ⧗ (M a) → (M b) → (M b)
+
+:test ((read >> (return 'a')) "hah") ("aah")
+
+# monadifies a list
+lift-m map ⧗ (a → b) → (M a) → (M b)
+
+# monadifies a list with two monadic arguments
+lift-m2 [[[concat ([[4 1 0] <$> 1] <$> 1)]]] ⧗ (a → b → c) → (M a) → (M b) → (M c)
+
+# evaluates monadic actions
+sequence foldr (lift-m2 cons) {}empty ⧗ (List (M a)) → (M (List a))
+
+>‣ [sequence ∘∘ 0]
+
+# traverses list based on modifier
+traverse sequence ∘∘ map ⧗ (a → (M b)) → (N a) → (M (N b))
+
+# performs action n times
+replicate-m >replicate ⧗ Number → (M a) → (M (List a))
+
+# maps elements to a monadic action
+map-m >map ⧗ (a → (M b)) → (List a) → (M (List b))
+