Added types for most combinators

1 files changed, 54 insertions, 56 deletions

diff --git a/std/Combinator.bruijn b/std/Combinator.bruijn
index 37fa504..4529853 100644
--- a/std/Combinator.bruijn
+++ b/std/Combinator.bruijn
@@ -1,90 +1,89 @@
 # MIT License, Copyright (c) 2022 Marvin Borner
 # Inspired by Raymond Smullyan: To Mock a Mockingbird
-# -> bird monickered combinators (they're still quite useful though!)
-
-# apply combinator
-a [[1 0]]
-
-…$… a
+# → bird monickered combinators (they're still quite useful though!)
 
 # bluebird combinator: function composition: (f ∘ g) x = f (g x)
-b [[[2 (1 0)]]]
+b [[[2 (1 0)]]] ⧗ (b → c) → (a → b) → a → c
 
 …∘… b
 
 # blackbird combinator: 2x function composition: (f ∘∘ g) x y = f (g x y)
-b' [[[[3 (2 1 0)]]]]
+b' [[[[3 (2 1 0)]]]] ⧗ (c → d) → (a → b → c) → a → b → d
 
 …∘∘… b'
 
 # bunting combinator: 3x function composition: (f ∘∘∘ g) x y z = f (g x y z)
-b'' [[[[[4 (3 2 1 0)]]]]]
+b'' [[[[[4 (3 2 1 0)]]]]] ⧗ (d → e) → (a → b → c → d) → a → b → c → e
 
 …∘∘∘… b''
 
 # becard combinator
-b''' [[[[3 (2 (1 0))]]]]
+b''' [[[[3 (2 (1 0))]]]] ⧗ (c → d) → (b → c) → (a → b) → a → d
 
-# cardinal combinator: reverse arguments: \f x y = f y z
-c [[[2 0 1]]]
+# cardinal combinator: flip arguments: \f x y = f y z
+c [[[2 0 1]]] ⧗ (a → b → c) → b → a → c
 
 \‣ c
 
 # cardinal once removed combinator
-c* [[[[3 2 0 1]]]]
+c* [[[[3 2 0 1]]]] ⧗ (a → c → b → d) → a → b → c → d
 
 # cardinal twice removed combinator
-c** [[[[[4 3 2 0 1]]]]]
+c** [[[[[4 3 2 0 1]]]]] ⧗ (a → b → d → c → e) → a → b → c → d → e
 
 # dove combinator
-d [[[[3 2 (1 0)]]]]
+d [[[[3 2 (1 0)]]]] ⧗ a → (b → c) → b → d
 
 # dickcissel combinator
-d' [[[[[4 3 2 (1 0)]]]]]
+d' [[[[[4 3 2 (1 0)]]]]] ⧗ (a → b → d → e) → a → b → (c → d) → c → e
 
 # dovekies combinator
-d'' [[[[[4 (3 2) (1 0)]]]]]
+d'' [[[[[4 (3 2) (1 0)]]]]] ⧗ (c → d → e) → (a → c) → a → (b → d) → b → e
 
 # eagle combinator
-e [[[[[4 3 (2 1 0)]]]]]
+e [[[[[4 3 (2 1 0)]]]]] ⧗ (a → d → e) → a → (b → c → d) → b → c → e
 
 # bald eagle combinator
-e' [[[[[[[6 (5 4 3) (2 1 0)]]]]]]]
+e' [[[[[[[6 (5 4 3) (2 1 0)]]]]]]] ⧗ (e → f → g) → (a → b → e) → a → b → (c → d → f) → c → d → g
 
 # finch combinator
-f [[[0 1 2]]]
+f [[[0 1 2]]] ⧗ a → b → (b → a → c) → c
 
 # finch once removed combinator
-f* [[[[3 0 1 2]]]]
+f* [[[[3 0 1 2]]]] ⧗ (c → b → a → d) → a → b → c → d
 
 # finch twice removed combinator
-f** [[[[[4 3 0 1 2]]]]]
+f** [[[[[4 3 0 1 2]]]]] ⧗ (a → d → c → b → e) → a → b → c → d → e
 
 # goldfinch combinator
-g [[[[3 0 (2 1)]]]]
+g [[[[3 0 (2 1)]]]] ⧗ (b → c → d) → (a → c) → a → b → d
 
 # hummingbird combinator
-h [[[2 1 0 1]]]
+h [[[2 1 0 1]]] ⧗ (a → b → a → c) → a → b → c
 
 # idiot combinator: identity
-i [0]
+# aside from obvious usage it's also used as abstraction crusher
+# to indicate that an argument isn't used
+i [0] ⧗ a → a
+
+# idiot once removed combinator: apply, $
+i* [[1 0]] ⧗ (a → b) → a → b
 
-# idiot once removed combinator
-i* [[1 0]]
+…$… i*
 
 # idiot twice removed combinator
-i** [[[2 1 0]]]
+i** [[[2 1 0]]] ⧗ (a → b → c) → a → b → c
 
 # jay combinator
-j [[[[3 2 (3 0 1)]]]]
+j [[[[3 2 (3 0 1)]]]] ⧗ (a → b → b) → a → b → a → b
 
 # kestrel combinator: const, true
-k [[1]]
+k [[1]] ⧗ a → b → a
 
 const k
 
 # kite combinator: const id, false
-ki [[0]]
+ki [[0]] ⧗ a → b → b
 
 # konstant mocker combinator
 km [[0 0]]
@@ -96,7 +95,7 @@ km' [[1 1]]
 l [[1 (0 0)]]
 
 # mockingbird/omega combinator
-m [0 0]
+m [0 0] ⧗ (a → b) → b
 
 ω m
 
@@ -104,51 +103,51 @@ m [0 0]
 m' [[1 0 (1 0)]]
 
 # owl combinator
-o [[0 (1 0)]]
+o [[0 (1 0)]] ⧗ ((a → b) → a) → (a → b) → b
 
 # omega combinator
 Ω ω ω
 
 # phoenix combinator: liftM2
 # alternative name: starling prime: s'
-φ [[[[3 (2 0) (1 0)]]]]
+φ [[[[3 (2 0) (1 0)]]]] ⧗ (b → c → d) → (a → b) → (a → c) → a → d
 
 # psi combinator: on
-ψ [[[[3 (2 1) (2 0)]]]]
+ψ [[[[3 (2 1) (2 0)]]]] ⧗ (b → b → c) → (a → b) → a → a → c
 
-# queer combinator: reverse function composition: (f , g) x = g (f x)
-q [[[1 (2 0)]]]
+# queer bird combinator: reverse function composition: (f , g) x = g (f x)
+q [[[1 (2 0)]]] ⧗ (a → b) → (b → c) → a → c
 
 …,… q
 
 # quixotic bird combinator
-q' [[[2 (0 1)]]]
+q' [[[2 (0 1)]]] ⧗ (b → c) → a → (a → b) → c
 
 # quizzical bird combinator
-q'' [[[1 (0 2)]]]
+q'' [[[1 (0 2)]]] ⧗ a → (b → c) → (a → b) → c
 
 # quirky bird combinator
-q''' [[[0 (2 1)]]]
+q''' [[[0 (2 1)]]] ⧗ (a → b) → a → (b → c) → c
 
 # quacky bird combinator
-q'''' [[[0 (1 2)]]]
+q'''' [[[0 (1 2)]]] ⧗ a → (a → b) → (b → c) → c
 
 # robin combinator
-r [[[1 0 2]]]
+r [[[1 0 2]]] ⧗ a → (b → a → c) → b → c
 
 # robin once removed combinator
-r* [[[[3 1 0 2]]]]
+r* [[[[3 1 0 2]]]] ⧗ (b → c → a → d) → a → b → c → d
 
 # robin twice removed combinator
-r** [[[[[4 3 1 0 2]]]]]
+r** [[[[[4 3 1 0 2]]]]] ⧗ (a → c → d → b → e) → a → b → c → d → e
 
 # starling combinator: (f <*> g) x = f x (g x)
-s [[[2 0 (1 0)]]]
+s [[[2 0 (1 0)]]] ⧗ (a → b → c) → (a → b) → a → c
 
 …<*>… s
 
 # thrush combinator: flipped $
-t [[0 1]]
+t [[0 1]] ⧗ a → (a → b) → b
 
 …&… t
 
@@ -156,32 +155,32 @@ t [[0 1]]
 u [[0 (1 1 0)]]
 
 # vireo combinator
-v [[[0 2 1]]]
+v [[[0 2 1]]] ⧗ a → b → (a → b → c) → c
 
 # vireo once removed combinator
-v* [[[[3 0 2 1]]]]
+v* [[[[3 0 2 1]]]] ⧗ (b → a → b → d) → a → b → b → d
 
 # vireo twice removed combinator
-v** [[[[[4 3 0 2 1]]]]]
+v** [[[[[4 3 0 2 1]]]]] ⧗ (a → c → b → c → e) → a → b → c → c → e
 
 # warbler combinator
-w [[1 0 0]]
+w [[1 0 0]] ⧗ (a → a → b) → a → b
 
 # warbler once removed combinator
-w* [[[2 1 0 0]]]
+w* [[[2 1 0 0]]] ⧗ (a → b → b → c) → a → b → c
 
 # warbler twice removed combinator
-w** [[[[3 2 1 0 0]]]]
+w** [[[[3 2 1 0 0]]]] ⧗ (a → b → c → c → d) → a → b → c → d
 
 # converse warbler combinator
-w' [[0 1 1]]
+w' [[0 1 1]] ⧗ a → (a → a → b) → b
 
 # sage bird combinator
-y [[1 (0 0)] [1 (0 0)]]
+y [[1 (0 0)] [1 (0 0)]] ⧗ (a → a) → a
 
 # z fixed point combinator
 # y and z are almost always interchangeable
-z [[1 [1 1 0]] [1 [1 1 0]]]
+z [[1 [1 1 0]] [1 [1 1 0]]] ⧗ (a → a) → a
 
 # theta combinator
 θ [[0 (1 1 0)]] [[0 (1 1 0)]]
@@ -191,7 +190,6 @@ z [[1 [1 1 0]] [1 [1 1 0]]]
 
 # -- combinator equivalency tests --
 
-:test (a) (s (s k))
 :test (b) (s (k s) k)
 :test (b') (b b b)
 :test (b'') (b (b b b) b)