aboutsummaryrefslogtreecommitdiffhomepage
path: root/std/Option.bruijn
diff options
context:
space:
mode:
authorMarvin Borner2023-02-23 10:49:13 +0100
committerMarvin Borner2023-02-23 10:49:13 +0100
commitc11a39217ac9e0a166442a634692114343a484ee (patch)
tree4d6f5e16ce0ed08a7ff61bfd0660351851d4b99b /std/Option.bruijn
parent0cb2b27268b637f5f87c797ba3982f64ec4bbd4c (diff)
Fixed and typed result/option monads
Diffstat (limited to 'std/Option.bruijn')
-rw-r--r--std/Option.bruijn17
1 files changed, 9 insertions, 8 deletions
diff --git a/std/Option.bruijn b/std/Option.bruijn
index b48fdc2..c0d57b4 100644
--- a/std/Option.bruijn
+++ b/std/Option.bruijn
@@ -1,45 +1,46 @@
# MIT License, Copyright (c) 2022 Marvin Borner
:import std/Combinator .
+:import std/Logic .
# empty option
-none true
+none true ⧗ (Option a)
# encapsulates value in option
-some [[[0 2]]]
+some [[[0 2]]] ⧗ (Option a)
# checks whether option is none
-none? [0 true [false]]
+none? [0 true [false]] ⧗ (Option a) → Boolean
:test (none? none) (true)
:test (none? (some [[0]])) (false)
# checks whether option is some
-some? [0 false [true]]
+some? [0 false [true]] ⧗ (Option a) → Boolean
:test (some? none) (false)
:test (some? (some [[0]])) (true)
# applies a function to the value in option
-map [[0 none [some (2 0)]]]
+map [[0 none [some (2 0)]]] ⧗ (a → b) → (Option a) → (Option b)
:test (map [[1]] (some [[0]])) (some [[[0]]])
:test (map [[1]] none) (none)
# applies a function to the value in option or returns first arg if none
-map-or [[[0 2 1]]]
+map-or [[[0 2 1]]] ⧗ (a → b) → (Option a) → (Option c)
:test (map-or [[[2]]] [[1]] (some [[0]])) ([[[0]]])
:test (map-or [[[2]]] [[1]] none) ([[[2]]])
# extracts value from option or returns first argument if none
-unwrap-or [[0 1 I]]
+unwrap-or [[0 1 i]] ⧗ a → (Option b) → c
:test (unwrap-or false (some true)) (true)
:test (unwrap-or false none) (false)
# applies encapsulated value to given function
-apply [[1 none 0]]
+apply [[1 none 0]] ⧗ (Option a) → (a → b) → c
:test (apply none [some ([[1]] 0)]) (none)
:test (apply (some [[0]]) [some ([[1]] 0)]) (some [[[0]]])