Standard library sync

8 files changed, 169 insertions, 114 deletions

diff --git a/std/Byte.bruijn b/std/Byte.bruijn
index 36aaf58..8dcbb7b 100644
--- a/std/Byte.bruijn
+++ b/std/Byte.bruijn
@@ -11,7 +11,7 @@ b0 false
 b1 true
 
 # returns true if two bytes are equal
-eq? &&‣ .. (zip-with xnor?)
+eq? ⋀?‣ ∘∘ (zip-with xnor?)
 
 …=?… eq?
 
diff --git a/std/Church.bruijn b/std/Church.bruijn
index 6277dcc..9e567b0 100644
--- a/std/Church.bruijn
+++ b/std/Church.bruijn
@@ -2,6 +2,12 @@
 
 zero [[0]]
 
+zero? [0 [[[0]]] [[1]]]
+
+dec [[[2 [[0 (1 3)]] [1] [0]]]]
+
+--‣ dec
+
 inc [[[1 (2 1 0)]]]
 
 ++‣ inc
@@ -12,7 +18,7 @@ add [[[[3 1 (2 1 0)]]]]
 
 mul [[[2 (1 0)]]]
 
-…*… mul
+…⋅… mul
 
 exp [[0 1]]
 
diff --git a/std/Combinator.bruijn b/std/Combinator.bruijn
index 34f9631..37fa504 100644
--- a/std/Combinator.bruijn
+++ b/std/Combinator.bruijn
@@ -180,6 +180,7 @@ w' [[0 1 1]]
 y [[1 (0 0)] [1 (0 0)]]
 
 # z fixed point combinator
+# y and z are almost always interchangeable
 z [[1 [1 1 0]] [1 [1 1 0]]]
 
 # theta combinator
diff --git a/std/List.bruijn b/std/List.bruijn
index f0cbc47..bce9463 100644
--- a/std/List.bruijn
+++ b/std/List.bruijn
@@ -12,9 +12,9 @@ empty false
 # returns true if a list is empty
 empty? [0 [[[false]]] true]
 
-<>?‣ empty?
+∅?‣ empty?
 
-:test (<>?empty) (true)
+:test (∅?empty) (true)
 
 # prepends an element to a list
 cons P.pair
@@ -22,7 +22,7 @@ cons P.pair
 …:… cons
 
 :test ((+1) : ((+2) : empty)) (P.pair (+1) (P.pair (+2) empty))
-:test (<>?((+2) : empty)) (false)
+:test (∅?((+2) : empty)) (false)
 
 # returns the head of a list or empty
 head P.fst
@@ -40,18 +40,18 @@ tail P.snd
 
 # returns the length of a list in balanced ternary
 length z [[[rec]]] (+0)
-	rec <>?0 case-end case-inc
+	rec ∅?0 case-end case-inc
 		case-inc 2 ++1 ~0
 		case-end 1
 
-#‣ length
+∀‣ length
 
-:test (#((+1) : ((+2) : empty))) ((+2))
-:test (#empty) ((+0))
+:test (∀((+1) : ((+2) : empty))) ((+2))
+:test (∀empty) ((+0))
 
 # returns the element at index in list
 index z [[[rec]]]
-	rec <>?0 case-end case-index
+	rec ∅?0 case-end case-index
 		case-index =?1 ^0 (2 --1 ~0)
 		case-end empty
 
@@ -64,7 +64,7 @@ index z [[[rec]]]
 
 # applies a left fold on a list
 foldl z [[[[rec]]]]
-	rec <>?0 case-end case-fold
+	rec ∅?0 case-end case-fold
 		case-fold 3 2 (2 1 ^0) ~0
 		case-end 1
 
@@ -76,7 +76,7 @@ foldl1 [[foldl 1 ^0 ~0]]
 
 # applies a right fold on a list
 foldr [[[z [[rec]] 0]]]
-	rec <>?0 case-end case-fold
+	rec ∅?0 case-end case-fold
 		case-fold 4 ^0 (1 ~0)
 		case-end 3
 
@@ -124,7 +124,7 @@ singleton [0 : empty]
 
 # appends two lists
 append z [[[rec]]]
-	rec <>?1 case-end case-append
+	rec ∅?1 case-end case-append
 		case-append ^1 : (2 ~1 0)
 		case-end 0
 
@@ -142,7 +142,7 @@ snoc [[1 ++ ({ 0 })]]
 
 # maps each element to a function
 map z [[[rec]]]
-	rec <>?0 case-end case-map
+	rec ∅?0 case-end case-map
 		case-map (1 ^0) : (2 1 ~0)
 		case-end empty
 
@@ -152,7 +152,7 @@ map z [[[rec]]]
 
 # filters a list based on a predicate
 filter z [[[rec]]]
-	rec <>?0 case-end case-filter
+	rec ∅?0 case-end case-filter
 		case-filter 1 ^0 (cons ^0) i (2 1 ~0)
 		case-end empty
 
@@ -163,20 +163,20 @@ filter z [[[rec]]]
 # returns the last element of a list
 # - slow algorithm:
 #   last z [[rec]]
-#   	rec <>?0 case-end case-last
-#   		case-last <>?(~0) ^0 (1 ~0)
+#   	rec ∅?0 case-end case-last
+#   		case-last ∅?(~0) ^0 (1 ~0)
 #   		case-end empty
 # - taking the first element of the reversed list is actually way faster because laziness
 last ^‣ ∘ <~>‣
 
 _‣ last
 
-:test (last ((+1) : ((+2) : ((+3) : empty)))) ((+3))
+:test (_((+1) : ((+2) : ((+3) : empty)))) ((+3))
 
 # returns everything but the last element of a list
 init z [[rec]]
-	rec <>?0 case-end case-init
-		case-init <>?(~0) empty (^0 : (1 ~0))
+	rec ∅?0 case-end case-init
+		case-init ∅?(~0) empty (^0 : (1 ~0))
 		case-end empty
 
 :test (init ((+1) : ((+2) : ((+3) : empty)))) ((+1) : ((+2) : empty))
@@ -196,16 +196,16 @@ concat-map concat ∘∘ map
 
 # zips two lists discarding excess elements
 zip z [[[rec]]]
-	rec <>?1 case-end case-zip
-		case-zip <>?0 empty ((^1 : ^0) : (2 ~1 ~0))
+	rec ∅?1 case-end case-zip
+		case-zip ∅?0 empty ((^1 : ^0) : (2 ~1 ~0))
 		case-end empty
 
 :test (zip ((+1) : ((+2) : empty)) ((+2) : ((+1) : empty))) (((+1) : (+2)) : (((+2) : (+1)) : empty))
 
 # applies pairs of the zipped list as arguments to a function
 zip-with z [[[[rec]]]]
-	rec <>?1 case-end case-zip
-		case-zip <>?0 empty ((2 ^1 ^0) : (3 2 ~1 ~0))
+	rec ∅?1 case-end case-zip
+		case-zip ∅?0 empty ((2 ^1 ^0) : (3 2 ~1 ~0))
 		case-end empty
 
 :test (zip-with …+… ((+1) : ((+2) : empty)) ((+2) : ((+1) : empty))) ((+3) : ((+3) : empty))
@@ -222,7 +222,7 @@ zip-with z [[[[rec]]]]
 
 # returns first n elements of a list
 take z [[[rec]]]
-	rec <>?0 case-end case-take
+	rec ∅?0 case-end case-take
 		case-take =?1 empty (^0 : (2 --1 ~0))
 		case-end empty
 
@@ -230,7 +230,7 @@ take z [[[rec]]]
 
 # takes elements while a predicate is satisfied
 take-while z [[[rec]]]
-	rec <>?0 case-end case-take
+	rec ∅?0 case-end case-take
 		case-take 1 ^0 (^0 : (2 1 ~0)) empty
 		case-end empty
 
@@ -238,7 +238,7 @@ take-while z [[[rec]]]
 
 # removes first n elements of a list
 drop z [[[rec]]]
-	rec <>?0 case-end case-drop
+	rec ∅?0 case-end case-drop
 		case-drop =?1 0 (2 --1 ~0)
 		case-end empty
 
@@ -246,7 +246,7 @@ drop z [[[rec]]]
 
 # removes elements from list while a predicate is satisfied
 drop-while z [[[rec]]]
-	rec <>?0 case-end case-drop
+	rec ∅?0 case-end case-drop
 		case-drop 1 ^0 (2 1 ~0) 0
 		case-end empty
 
@@ -254,7 +254,7 @@ drop-while z [[[rec]]]
 
 # returns pair of take-while and drop-while
 span z [[[rec]]]
-	rec <>?0 case-end case-drop
+	rec ∅?0 case-end case-drop
 		case-drop 1 ^0 ((^0 : ^recced) : ~recced) (empty : 0)
 			recced 2 1 ~0
 		case-end empty : empty
@@ -266,6 +266,16 @@ break span ∘ (…∘… ¬‣)
 
 :test (break (\gre? (+3)) ((+1) : ((+2) : ((+4) : ((+1) : empty))))) (((+1) : ((+2) : empty)) : ((+4) : ((+1) : empty)))
 
+# splits a list into two lists based on predicate
+split-at z [[[rec]]]
+	rec ∅?dropped case-end case-split
+		dropped drop-while 1 0
+		case-split ^broken : (2 1 ~broken)
+			broken break 1 dropped
+		case-end empty
+
+:test (split-at (…=?… (+1)) ((+2) : ((+1) : ((+3) : ((+2) : empty))))) ((((+2) : empty) : (((+3) : ((+2) : empty)) : empty)))
+
 # returns true if any element in a list matches a predicate
 any? ⋁?‣ ∘∘ map
 
@@ -293,7 +303,7 @@ eq? ⋀?‣ ∘∘∘ zip-with
 
 # removes first element that match an eq predicate
 remove z [[[[rec]]]]
-	rec <>?0 case-end case-remove
+	rec ∅?0 case-end case-remove
 		case-remove (2 ^0 1) ~0 (^0 : (3 2 1 ~0))
 		case-end empty
 
@@ -301,7 +311,7 @@ remove z [[[[rec]]]]
 
 # removes duplicates from list based on eq predicate (keeps first occurrence)
 nub z [[[rec]]]
-	rec <>?0 case-end case-nub
+	rec ∅?0 case-end case-nub
 		case-nub ^0 : (2 1 (~0 <#> [¬(2 0 ^1)]))
 		case-end empty
 
@@ -330,6 +340,6 @@ iterate z [[[rec]]]
 	rec 0 : (2 1 (1 0))
 
 :test (take (+5) (iterate ++‣ (+0))) (((+0) : ((+1) : ((+2) : ((+3) : ((+4) : empty))))))
-:test (take (+2) (iterate sdec (+5))) (((+5) : ((+4) : empty)))
+:test (take (+2) (iterate (%‣ ∘ dec) (+5))) (((+5) : ((+4) : empty)))
 :test (take (+5) (iterate i (+4))) (take (+5) (repeat (+4)))
 :test (take (+0) (iterate ++‣ (+0))) (empty)
diff --git a/std/Math.bruijn b/std/Math.bruijn
index 9d3dff2..7cf0af0 100644
--- a/std/Math.bruijn
+++ b/std/Math.bruijn
@@ -1,7 +1,6 @@
 # MIT License, Copyright (c) 2022 Marvin Borner
 
 :import std/List .
-
 :input std/Number .
 
 # adds all values in list
@@ -69,6 +68,23 @@ pow […!!… (iterate (…*… 0) (+1))]
 
 :test (((+2) ** (+3)) =? ((+8))) (true)
 
+# power function using ternary exponentiation
+# a 1 → b 0
+# pow' z [[[rec]]]
+# 	rec =?0 case-end case-pow
+# 		case-pow =?(lst 0) (mult ⊩r) ((mult ⊩r) ⋅ 1)
+# 			mult [0 ⋅ 0 ⋅ 0]
+# 			r 2 1 /³0
+# 		case-end (+1)
+pow' z [[[rec]]]
+	rec =?0 case-end case-pow
+		case-pow =?(lst 0) (r ⋅ r ⋅ r) (r ⋅ r ⋅ r ⋅ 1)
+			r 2 1 /³0
+		case-end (+1)
+
+# prime number sequence
+primes nub ((…≠?… (+1)) ∘∘ gcd) (iterate ++‣ (+2))
+
 # factorial function
 # TODO: faster fac?
 fac [∏ (+1) → 0 | i]
@@ -82,3 +98,20 @@ fibs fst <$> (iterate [~0 : (^0 + ~0)] ((+0) : (+1)))
 fib [fibs !! ++0]
 
 :test (fib (+5)) ((+8))
+
+# pascal triangle
+# TODO: this generally works, BUT lists in lists get reduced and mess up indexing
+pascal iterate [zip-with …+… ({ (+0) } ++ 0) (0 ; (+0))] ({ (+1) })
+
+# π
+# q 3, r 2, t 1, i 0
+# translation of unbounded spigot algorithm by Jeremy Gibbons
+π g (+1) (+180) (+60) (+2)
+	g y [[[[[calc]]]]]
+		calc b : (4 q r t i)
+			a ↑⁰(↑⁺0 ⋅ (↑⁰0 + (+2)))
+			b (3 ⋅ ↑⁰(↑⁻(↑⁻0)) + ((+5) ⋅ 2)) /! ((+5) ⋅ 1)
+			q (+10) ⋅ 3 ⋅ 0 ⋅ --((+2) ⋅ 0)
+			r (+10) ⋅ a ⋅ (3 ⋅ ((+5) ⋅ 0 - (+2)) + 2 - (b ⋅ 1)
+			t 1 ⋅ a
+			i ++0
diff --git a/std/Number.bruijn b/std/Number.bruijn
index ae4a3ac..3a2efe9 100644
--- a/std/Number.bruijn
+++ b/std/Number.bruijn
@@ -8,22 +8,22 @@
 :import std/Logic .
 
 # negative trit indicating coeffecient of (-1)
-t⁻ [[[2]]]
+t⁻ [[[2]]] ⧗ Trit
 
 # returns true if a trit is negative
-t⁻? [0 true false false]
+t⁻? [0 true false false] ⧗ Trit → Boolean
 
 # positive trit indicating coeffecient of (+1)
-t⁺ [[[1]]]
+t⁺ [[[1]]] ⧗ Trit
 
 # returns true if a trit is positive
-t⁺? [0 false true false]
+t⁺? [0 false true false] ⧗ Trit → Boolean
 
 # zero trit indicating coeffecient of 0
-t⁰ [[[0]]]
+t⁰ [[[0]]] ⧗ Trit
 
 # returns true if a trit is zero
-t⁰? [0 false false true]
+t⁰? [0 false false true] ⧗ Trit → Boolean
 
 :test (t⁻? t⁻) (true)
 :test (t⁻? t⁺) (false)
@@ -36,28 +36,28 @@ t⁰? [0 false false true]
 :test (t⁰? t⁰) (true)
 
 # shifts a negative trit into a balanced ternary number
-↑⁻‣ [[[[[2 (4 3 2 1 0)]]]]]
+↑⁻‣ [[[[[2 (4 3 2 1 0)]]]]] ⧗ Number → Number
 
 :test (↑⁻(+0)) ((-1))
 :test (↑⁻(-1)) ((-4))
 :test (↑⁻(+42)) ((+125))
 
 # shifts a positive trit into a balanced ternary number
-↑⁺‣ [[[[[1 (4 3 2 1 0)]]]]]
+↑⁺‣ [[[[[1 (4 3 2 1 0)]]]]] ⧗ Number → Number
 
 :test (↑⁺(+0)) ((+1))
 :test (↑⁺(-1)) ((-2))
 :test (↑⁺(+42)) ((+127))
 
 # shifts a zero trit into a balanced ternary number
-↑⁰‣ [[[[[0 (4 3 2 1 0)]]]]]
+↑⁰‣ [[[[[0 (4 3 2 1 0)]]]]] ⧗ Number → Number
 
 :test (↑⁰(+0)) ([[[[0 3]]]])
 :test (↑⁰(+1)) ((+3))
 :test (↑⁰(+42)) ((+126))
 
 # shifts a specified trit into a balanced ternary number
-up [[[[[[5 2 1 0 (4 3 2 1 0)]]]]]]
+up [[[[[[5 2 1 0 (4 3 2 1 0)]]]]]] ⧗ Trit → Number → Number
 
 :test (up t⁻ (+42)) (↑⁻(+42))
 :test (up t⁺ (+42)) (↑⁺(+42))
@@ -65,10 +65,10 @@ up [[[[[[5 2 1 0 (4 3 2 1 0)]]]]]]
 
 # infinity
 # WARNING: using this mostly results in undefined behavior! (TODO?)
-infty z [[[[[1 (4 1)]]]]]
+infty z [[[[[1 (4 1)]]]]] ⧗ Number
 
 # negates a balanced ternary number
-negate [[[[[4 3 1 2 0]]]]]
+negate [[[[[4 3 1 2 0]]]]] ⧗ Number → Number
 
 -‣ negate
 
@@ -77,7 +77,7 @@ negate [[[[[4 3 1 2 0]]]]]
 :test (-(+42)) ((-42))
 
 # converts a balanced ternary number to a list of trits
-list! [0 z a⁻ a⁺ a⁰]
+list! [0 z a⁻ a⁺ a⁰] ⧗ Number → List
 	z [[0]]
 	a⁻ [t⁻ : 0]
 	a⁺ [t⁺ : 0]
@@ -86,7 +86,7 @@ list! [0 z a⁻ a⁺ a⁰]
 # TODO: Tests!
 
 # strips leading 0s from balanced ternary number
-strip [^(0 z a⁻ a⁺ a⁰)]
+strip [^(0 z a⁻ a⁺ a⁰)] ⧗ Number → Number
 	z (+0) : true
 	a⁻ [0 [[↑⁻1 : false]]]
 	a⁺ [0 [[↑⁺1 : false]]]
@@ -99,15 +99,15 @@ strip [^(0 z a⁻ a⁺ a⁰)]
 :test (%(+42)) ((+42))
 
 # extracts least significant trit from balanced ternary numbers
-lst [0 t⁰ [t⁻] [t⁺] [t⁰]]
+lst [0 t⁰ [t⁻] [t⁺] [t⁰]] ⧗ Number → Trit
 
 :test (lst (-1)) (t⁻)
 :test (lst (+0)) (t⁰)
 :test (lst (+1)) (t⁺)
 :test (lst (+42)) (t⁰)
 
-# checks true if balanced ternary number is zero
-zero? [0 true [false] [false] i]
+# returns true if balanced ternary number is zero
+zero? [0 true [false] [false] i] ⧗ Number → Boolean
 
 =?‣ zero?
 
@@ -116,11 +116,21 @@ zero? [0 true [false] [false] i]
 :test (=?(+1)) (false)
 :test (=?(+42)) (false)
 
+# returns true if balanced ternary number is not
+not-zero? [0 false [true] [true] i] ⧗ Number → Boolean
+
+≠?‣ not-zero?
+
+:test (≠?(+0)) (false)
+:test (≠?(-1)) (true)
+:test (≠?(+1)) (true)
+:test (≠?(+42)) (true)
+
 # extracts most significant trit from balanced ternary numbers
 # <~>/<>? are hardcoded because list import would be recursive (TODO?)
 # while this looks incredibly inefficient it's actually fairly fast because laziness
 # TODO: find way of removing requirement of stripping first
-mst [=?0 t⁰ ^(<~>(list! %0))]
+mst [=?0 t⁰ ^(<~>(list! %0))] ⧗ Number → Trit
 	<~>‣ z [[[[<>?0 1 (3 2 (2 1 ^0) ~0)]]]] f false
 		<>?‣ [0 [[[false]]] true]
 
@@ -130,7 +140,7 @@ mst [=?0 t⁰ ^(<~>(list! %0))]
 :test (mst (+42)) (t⁺)
 
 # returns true if balanced ternary number is negative
-negative? [t⁻? (mst 0)]
+negative? [t⁻? (mst 0)] ⧗ Number → Boolean
 
 <?‣ negative?
 
@@ -140,7 +150,7 @@ negative? [t⁻? (mst 0)]
 :test (<?(+42)) (false)
 
 # returns true if balanced ternary number is positive
-positive? [t⁺? (mst 0)]
+positive? [t⁺? (mst 0)] ⧗ Number → Boolean
 
 >?‣ positive?
 
@@ -152,7 +162,7 @@ positive? [t⁺? (mst 0)]
 # converts the normal balanced ternary representation into abstract
 # infinity can't be abstracted in finite time
 # → the abstract representation is used in eq?/add/sub/mul
-abstract! [0 z a⁻ a⁺ a⁰]
+abstract! [0 z a⁻ a⁺ a⁰] ⧗ Number → AbstractNumber
 	z (+0)
 	a⁻ [[[[[2 4]]]]]
 	a⁺ [[[[[1 4]]]]]
@@ -165,7 +175,7 @@ abstract! [0 z a⁻ a⁺ a⁰]
 :test (→^(+3)) ([[[[0 [[[[1 [[[[3]]]]]]]]]]]])
 
 # converts the abstracted balanced ternary representation back to normal
-normal! ω [[0 z a⁻ a⁺ a⁰]]
+normal! ω [[0 z a⁻ a⁺ a⁰]] ⧗ AbstractNumber → Number
 	z (+0)
 	a⁻ [↑⁻([3 3 0] 0)]
 	a⁺ [↑⁺([3 3 0] 0)]
@@ -177,10 +187,10 @@ normal! ω [[0 z a⁻ a⁺ a⁰]]
 :test (→_(→^(+42))) ((+42))
 :test (→_(→^(-42))) ((-42))
 
-# checks whether two balanced ternary numbers are equal
+# returns true if two balanced ternary numbers are equal
 # larger numbers should be second argument (performance)
 # → ignores leading 0s!
-eq? [[abs 1 →^0]]
+eq? [[abs 1 →^0]] ⧗ Number → Number → Boolean
 	abs [0 z a⁻ a⁺ a⁰]
 		z [=?(→_0)]
 		a⁻ [[0 false [2 0] [false] [false]]]
@@ -189,9 +199,9 @@ eq? [[abs 1 →^0]]
 
 …=?… eq?
 
-neq? not! ∘∘ eq?
+not-eq? not! ∘∘ eq? ⧗ Number → Number → Boolean
 
-…/=?… neq?
+…≠?… not-eq?
 
 :test ((-42) =? (-42)) (true)
 :test ((-1) =? (-1)) (true)
@@ -201,8 +211,8 @@ neq? not! ∘∘ eq?
 :test ((+1) =? (+1)) (true)
 :test ((+42) =? (+42)) (true)
 :test ([[[[(1 (0 (0 (0 (0 3)))))]]]] =? (+1)) (true)
-:test ((+1) /=? (+0)) (true)
-:test ((-42) /=? (+42)) (true)
+:test ((+1) ≠? (+0)) (true)
+:test ((-42) ≠? (+42)) (true)
 
 # I believe Mogensen's Paper has an error in its inc/dec/add/mul/eq definitions.
 # They use 3 instead of 2 abstractions in the functions, also we use switched
@@ -210,7 +220,7 @@ neq? not! ∘∘ eq?
 # the same. Something's weird.
 
 # adds (+1) to a balanced ternary number (can introduce leading 0s)
-inc [~(0 z a⁻ a⁺ a⁰)]
+inc [~(0 z a⁻ a⁺ a⁰)] ⧗ Number → Number
 	z (+0) : (+1)
 	a⁻ [0 [[↑⁻1 : ↑⁰1]]]
 	a⁺ [0 [[↑⁺1 : ↑⁻0]]]
@@ -218,9 +228,6 @@ inc [~(0 z a⁻ a⁺ a⁰)]
 
 ++‣ inc
 
-# adds (+1) to a balanced ternary number and strips leading 0s
-ssinc strip ∘ inc
-
 :test ((++(-42)) =? (-41)) (true)
 :test ((++(-1)) =? (+0)) (true)
 :test ((++(+0)) =? (+1)) (true)
@@ -228,7 +235,7 @@ ssinc strip ∘ inc
 :test ((++(+42)) =? (+43)) (true)
 
 # subs (+1) from a balanced ternary number (can introduce leading 0s)
-dec [~(0 z a⁻ a⁺ a⁰)]
+dec [~(0 z a⁻ a⁺ a⁰)] ⧗ Number → Number
 	z (+0) : (-1)
 	a⁻ [0 [[↑⁻1 : ↑⁺0]]]
 	a⁺ [0 [[↑⁺1 : ↑⁰1]]]
@@ -236,9 +243,6 @@ dec [~(0 z a⁻ a⁺ a⁰)]
 
 --‣ dec
 
-# subs (+1) from a balanced ternary number and strips leading 0s
-sdec strip ∘ dec
-
 :test ((--(-42)) =? (-43)) (true)
 :test ((--(+0)) =? (-1)) (true)
 :test ((--(--(--(--(--(+5)))))) =? (+0)) (true)
@@ -247,7 +251,7 @@ sdec strip ∘ dec
 
 # adds two balanced ternary numbers (can introduce leading 0s)
 # second argument gets abstracted (performance)
-add [[abs 1 →^0]]
+add [[abs 1 →^0]] ⧗ Number → Number → Number
 	abs [c (0 z a⁻ a⁺ a⁰)]
 		b⁻ [1 ↑⁺(3 0 t⁻) ↑⁰(3 0 t⁰) ↑⁻(3 0 t⁰)]
 		b⁰ [up 1 (3 0 t⁰)]
@@ -262,9 +266,6 @@ add [[abs 1 →^0]]
 
 …+… add
 
-# adds two balanced ternary numbers and strips leading 0s
-sadd strip ∘∘ add
-
 :test (((-42) + (-1)) =? (-43)) (true)
 :test (((-5) + (+6)) =? (+1)) (true)
 :test (((-1) + (+0)) =? (-1)) (true)
@@ -274,13 +275,10 @@ sadd strip ∘∘ add
 
 # subs two balanced ternary numbers (can introduce leading 0s)
 # second argument gets abstracted (performance)
-sub [[1 + -0]]
+sub [[1 + -0]] ⧗ Number → Number → Number
 
 …-… sub
 
-# subs two balanced ternary numbers and strips leading 0s
-ssub strip ∘∘ sub
-
 :test (((-42) - (-1)) =? (-41)) (true)
 :test (((-5) - (+6)) =? (-11)) (true)
 :test (((-1) - (+0)) =? (-1)) (true)
@@ -290,7 +288,7 @@ ssub strip ∘∘ sub
 
 # returns true if number is greater than other number
 # larger numbers should be second argument (performance)
-gre? [[>?(1 - 0)]]
+gre? [[>?(1 - 0)]] ⧗ Number → Number → Boolean
 
 …>?… gre?
 
@@ -300,7 +298,7 @@ gre? [[>?(1 - 0)]]
 
 # returns true if number is less than other number
 # smaller numbers should be second argument (performance)
-les? \gre?
+les? \gre? ⧗ Number → Number → Boolean
 
 …<?… les?
 
@@ -310,7 +308,7 @@ les? \gre?
 
 # returns true if number is less than or equal to other number
 # smaller numbers should be second argument (performance)
-leq? [[¬(1 >? 0)]]
+leq? [[¬(1 >? 0)]] ⧗ Number → Number → Boolean
 
 …≤?… leq?
 
@@ -320,7 +318,7 @@ leq? [[¬(1 >? 0)]]
 
 # returns true if number is greater than or equal to other number
 # smaller numbers should be second argument (performance)
-geq? \leq?
+geq? \leq? ⧗ Number → Number → Boolean
 
 …≥?… geq?
 
@@ -329,7 +327,7 @@ geq? \leq?
 :test ((+3) ≥? (+2)) (true)
 
 # negates a balanced ternary number if <0
-abs [<?0 -0 0]
+abs [<?0 -0 0] ⧗ Number → Number
 
 |‣ abs
 
@@ -337,24 +335,31 @@ abs [<?0 -0 0]
 :test (|(-1)) ((+1))
 :test (|(+42)) ((+42))
 
+# apply a function n times to a value
+# ~> substitute church numbers
+apply z [[[rec]]] ⧗ Number → (a → a) → a → a
+	rec =?1 case-end case-apply
+		case-apply 0 ∘ (2 --1 0)
+		case-end i
+
+:test (apply (+5) ++‣ (+3)) ((+8))
+
 # muls two balanced ternary numbers (can introduce leading 0s)
-mul [[1 z a⁻ a⁺ a⁰]]
+mul [[1 z a⁻ a⁺ a⁰]] ⧗ Number → Number → Number
 	z (+0)
 	a⁻ [↑⁰0 - 1]
 	a⁺ [↑⁰0 + 1]
 	a⁰ [↑⁰0]
 
-…*… mul
-
-smul strip ∘∘ mul
+…⋅… mul
 
-:test (((+42) * (+0)) =? (+0)) (true)
-:test (((-1) * (+42)) =? (-42)) (true)
-:test (((+3) * (+11)) =? (+33)) (true)
-:test (((+42) * (-4)) =? (-168)) (true)
+:test (((+42) ⋅ (+0)) =? (+0)) (true)
+:test (((-1) ⋅ (+42)) =? (-42)) (true)
+:test (((+3) ⋅ (+11)) =? (+33)) (true)
+:test (((+42) ⋅ (-4)) =? (-168)) (true)
 
 # divs a balanced ternary number by three (rshifts least significant trit)
-div³ [~(0 z a⁻ a⁺ a⁰)]
+div³ [~(0 z a⁻ a⁺ a⁰)] ⧗ Number → Number
 	z (+0) : (+0)
 	a⁻ [0 [[↑⁻1 : 1]]]
 	a⁺ [0 [[↑⁺1 : 1]]]
@@ -367,7 +372,7 @@ div³ [~(0 z a⁻ a⁺ a⁰)]
 :test (/³(+5)) ((+2))
 
 # divs a balanced ternary number by two (essentially binary >>1)
-div² [z [[[[rec]]]] (+0) 0 0]
+div² [z [[[[rec]]]] (+0) 0 0] ⧗ Number → Number
 	rec =?1 case-end case-div
 		case-div 3 /³(2 + 0) /³1 0
 		case-end 2
@@ -381,7 +386,7 @@ div² [z [[[[rec]]]] (+0) 0 0]
 # manually counts how many times a balanced ternary number fits into another one
 # TODO: quadratic approximation?
 # TODO: fix for negative numbers
-brute-div \[z [[[[[rec]]]]] (+0) 0 0]
+brute-div \[z [[[[[rec]]]]] (+0) 0 0] ⧗ Number → Number → Number
 	rec (2 >? 0) case-end case-count
 		case-count 4 ++3 (2 + 1) 1 0
 		case-end 3
@@ -393,16 +398,20 @@ brute-div \[z [[[[[rec]]]]] (+0) 0 0]
 :test ((+4) /! (+5)) ((+0))
 
 # TODO: fix for negative numbers
-brute-mod \[z [[[[[rec]]]]] (+0) 0 0]
+brute-mod \[z [[[[[rec]]]]] (+0) 0 0] ⧗ Number → Number → Number
 	rec (2 >? 0) case-end case-count
 		case-count 4 ++3 (2 + 1) 1 0
-		case-end 0 - (3 * 1)
+		case-end 0 - (3 ⋅ 1)
 
 …%!… brute-mod
 
 # finds quotient and remainder using long division
 # WARNING: don't use; incorrect and slow
-quot-rem [[z [[[[rec]]]] ((+1) : (+0)) 1 0]]
+# TODO: faster algorithm
+# dividend -> divisor -> (quot, rem)
+# 0 divisor, 1 dividend, 2 (quot, rem)
+# align: (quot, divisor)
+quot-rem [[z [[[[rec]]]] ((+1) : (+0)) 1 0]] ⧗ Number → Number → (Pair Number Number)
 	rec (1 =? 0) case-eq ((1 <? 0) case-les case-div)
 		case-div calc (z [[[align]]] ^2 0)
 			align (0 ≤? 4) (1 : 0) (2 ↑⁰1 ↑⁰0)
@@ -413,18 +422,18 @@ quot-rem [[z [[[[rec]]]] ((+1) : (+0)) 1 0]]
 
 # divs two balanced ternary numbers
 # WARNING: don't use; incorrect and slow
-div ^‣ ∘∘ quot-rem
+div ^‣ ∘∘ quot-rem ⧗ Number → Number
 
 …/… div
 
 # returns remainder of integer division
 # WARNING: don't use; incorrect and slow
-mod ~‣ ∘∘ quot-rem
+mod ~‣ ∘∘ quot-rem ⧗ Number → Number
 
 …%… mod
 
 # returns max number of two
-max [[(1 ≤? 0) 0 1]]
+max [[(1 ≤? 0) 0 1]] ⧗ Number → Number → Number
 
 # returns min number of two
-min [[(1 ≤? 0) 1 0]]
+min [[(1 ≤? 0) 1 0]] ⧗ Number → Number → Number
diff --git a/std/Pair.bruijn b/std/Pair.bruijn
index 7cc93fb..a955fe2 100644
--- a/std/Pair.bruijn
+++ b/std/Pair.bruijn
@@ -3,45 +3,45 @@
 :import std/Combinator .
 
 # pairs two expressions into one
-pair [[[0 2 1]]]
+pair [[[0 2 1]]] ⧗ a → b → (Pair a b)
 
 …:… pair
 
 # extracts first expression from pair
-fst [0 k]
+fst [0 k] ⧗ (Pair a b) → a
 
 ^‣ fst
 
 :test (^([[0]] : [[1]])) ([[0]])
 
 # extracts second expression from pair
-snd [0 ki]
+snd [0 ki] ⧗ (Pair a b) → b
 
 ~‣ snd
 
 :test (~([[0]] : [[1]])) ([[1]])
 
 # applies both elements of a pair to a function
-uncurry [[1 ^0 ~0]]
+uncurry [[1 ^0 ~0]] ⧗ (a → b → c) → (Pair a b) → c
 
 :test (uncurry w ([[0]] : [[1]])) ([[1]])
 
 # applies a function to the pair of two values
-curry [[[2 (1 : 0)]]]
+curry [[[2 (1 : 0)]]] ⧗ ((Pair a b) → c) → a → b → c
 
 :test (curry fst [[0]] [[1]]) ([[0]])
 
 # zips two pairs (basically rotating the elements)
-zip [[(^1 : ^0) : (~1 : ~0)]]
+zip [[(^1 : ^0) : (~1 : ~0)]] ⧗ (Pair a b) → (Pair c d) → (Pair (Pair a c) (Pair b d))
 
 :test (zip ([[0]] : [[[0]]]) ([[1]] : [[[1]]])) (([[0]] : [[1]]) : ([[[0]]] : [[[1]]]))
 
 # applies pairs of two pairs as arguments to a function
-zip-with [[[(2 ^1 ^0) : (2 ~1 ~0)]]]
+zip-with [[[(2 ^1 ^0) : (2 ~1 ~0)]]] ⧗ (a → b → c) → (Pair a b) → (Pair a b) → (Pair c c)
 
 :test (zip-with w ([[0]] : [[[0]]]) ([[1]] : [[[1]]])) ([[1]] : [0])
 
 # swaps the elements of a pair
-swap [~0 : ^0]
+swap [~0 : ^0] ⧗ (Pair a b) → (Pair b a)
 
 :test (swap ([[0]] : [[1]])) ([[1]] : [[0]])
diff --git a/std/String.bruijn b/std/String.bruijn
index bc80840..a288bac 100644
--- a/std/String.bruijn
+++ b/std/String.bruijn
@@ -28,16 +28,12 @@ ni? \in?
 
 # splits string by newline character
 lines z [[rec]]
-	rec <>?(~broken) (^broken : empty) (^broken : (1 ~(~broken)))
+	rec ∅?(~broken) (^broken : empty) (^broken : (1 ~(~broken)))
 		broken break (B.eq? '\n') 0
 
 :test (lines "ab\ncd") ("ab" : ("cd" : empty))
 
-# :test (lines "ab\ncd\n") ("ab" : ("cd" : empty))
-
 # concats list of strings with newline character
-unlines concat-map (\(;) '\n')
+unlines concat-map (\(…;…) '\n')
 
 :test (unlines ("ab" : ("cd" : empty))) ("ab\ncd\n")
-
-main lines "ab\ncd"