From e17ea13e7b94986af5d4b60ee6b83a34a0748249 Mon Sep 17 00:00:00 2001
From: Marvin Borner
Date: Fri, 6 Oct 2023 18:51:53 +0200
Subject: Fun with monads

---
 std/Monad.bruijn | 19 ++++++++++++++++++-
 1 file changed, 18 insertions(+), 1 deletion(-)

(limited to 'std/Monad.bruijn')

diff --git a/std/Monad.bruijn b/std/Monad.bruijn
index e015efa..97291eb 100644
--- a/std/Monad.bruijn
+++ b/std/Monad.bruijn
@@ -2,7 +2,7 @@
 # monadic interface for anything based on lists (e.g. IO, strings)
 # afaik originally proposed by John Tromp and inspired by Haskell
 
-:import std/Pair .
+:import std/List .
 :import std/Combinator .
 
 read [0] ⧗ a → (M a)
@@ -25,3 +25,20 @@ pure return ⧗ a → (M a)
 …>>… [[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]
+
+# 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))
-- 
cgit v1.2.3