diff options
Diffstat (limited to 'std')
-rw-r--r-- | std/IO.bruijn | 12 | ||||
-rw-r--r-- | std/Monad.bruijn | 49 | ||||
-rw-r--r-- | std/Monad/List.bruijn | 50 | ||||
-rw-r--r-- | std/Monad/State.bruijn | 12 |
4 files changed, 77 insertions, 46 deletions
diff --git a/std/IO.bruijn b/std/IO.bruijn new file mode 100644 index 0000000..fdc9295 --- /dev/null +++ b/std/IO.bruijn @@ -0,0 +1,12 @@ +# MIT License, Copyright (c) 2024 Marvin Borner + +:input std/Monad/List . + +:import std/Char C +:import std/Combinator . + +# reads a single char monadically +get-char read + +# reads a line monadically +get-line y [read >>= [(C.eq? 0 '\n') (pure [[0]]) (1 >>= [pure [0 2 1]])]] diff --git a/std/Monad.bruijn b/std/Monad.bruijn index 0dae29e..0feec73 100644 --- a/std/Monad.bruijn +++ b/std/Monad.bruijn @@ -1,47 +1,4 @@ -# 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 +# MIT License, Copyright (c) 2024 Marvin Borner +# just a reference to the list monad (default interface) -: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 -…>>=… [[[2 0 1]]] ⧗ (M a) → (a → (M b)) → (M a) - -: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)) +:input std/Monad/List 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)) + diff --git a/std/Monad/State.bruijn b/std/Monad/State.bruijn new file mode 100644 index 0000000..14c2669 --- /dev/null +++ b/std/Monad/State.bruijn @@ -0,0 +1,12 @@ +# MIT License, Copyright (c) 2024 Marvin Borner + +:import std/Combinator . + +# scala: s0 ⇒ { (s1, a) = run(s0); (s1, f(a)) } +map [[[1 0 [[[0 2 (5 1)]]]]]] ⧗ (a → b) → (State s a) → (State s b) + +# monadic bind/flat-map operator +# scala: s0 ⇒ { (s1, a) = run(s0); f(a).run(s1) } +bind [[[2 0 [[3 0 1]]]]] ⧗ (State s a) → (a → (State s b)) → (State s b) + +…>>=… bind |