From c11a39217ac9e0a166442a634692114343a484ee Mon Sep 17 00:00:00 2001
From: Marvin Borner
Date: Thu, 23 Feb 2023 10:49:13 +0100
Subject: Fixed and typed result/option monads

---
 std/Option.bruijn | 17 +++++++++--------
 1 file changed, 9 insertions(+), 8 deletions(-)

(limited to 'std/Option.bruijn')

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]]])
-- 
cgit v1.2.3