path: root/std/Combinator.bruijn

# MIT License, Copyright (c) 2022 Marvin Borner
# Inspired by Raymond Smullyan: To Mock a Mockingbird
# → bird monickered combinators (they're still quite useful though!)

# bluebird combinator: function composition: (f ∘ g) x = f (g x)
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)]]]] ⧗ (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)]]]]] ⧗ (d → e) → (a → b → c → d) → a → b → c → e

…∘∘∘… b''

# becard combinator
b''' [[[[3 (2 (1 0))]]]] ⧗ (c → d) → (b → c) → (a → b) → a → d

# cardinal combinator: flip arguments: \f x y = f y x
c [[[2 0 1]]] ⧗ (a → b → c) → b → a → c

\‣ c

# cardinal once removed combinator
c* [[[[3 2 0 1]]]] ⧗ (a → c → b → d) → a → b → c → d

# cardinal twice removed combinator
c** [[[[[4 3 2 0 1]]]]] ⧗ (a → b → d → c → e) → a → b → c → d → e

# dove combinator
d [[[[3 2 (1 0)]]]] ⧗ a → (b → c) → b → d

# dickcissel combinator
d' [[[[[4 3 2 (1 0)]]]]] ⧗ (a → b → d → e) → a → b → (c → d) → c → e

# dovekies combinator
d'' [[[[[4 (3 2) (1 0)]]]]] ⧗ (c → d → e) → (a → c) → a → (b → d) → b → e

# eagle combinator
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 → f → g) → (a → b → e) → a → b → (c → d → f) → c → d → g

# finch combinator
f [[[0 1 2]]] ⧗ a → b → (b → a → c) → c

# finch once removed combinator
f* [[[[3 0 1 2]]]] ⧗ (c → b → a → d) → a → b → c → d

# finch twice removed combinator
f** [[[[[4 3 0 1 2]]]]] ⧗ (a → d → c → b → e) → a → b → c → d → e

# goldfinch combinator
g [[[[3 0 (2 1)]]]] ⧗ (b → c → d) → (a → c) → a → b → d

# hummingbird combinator
h [[[2 1 0 1]]] ⧗ (a → b → a → c) → a → b → c

# idiot combinator: identity
# 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

…$… i*

# idiot twice removed combinator
i** [[[2 1 0]]] ⧗ (a → b → c) → a → b → c

# jay combinator
j [[[[3 2 (3 0 1)]]]] ⧗ (a → b → b) → a → b → a → b

# kestrel combinator: const, true
k [[1]] ⧗ a → b → a

const k

# kite combinator: const id, false
ki [[0]] ⧗ a → b → b

# konstant mocker combinator
km [[0 0]]

# crossed konstant mocker combinator
km' [[1 1]]

# lark combinator
l [[1 (0 0)]]

# mockingbird/omega combinator
m [0 0] ⧗ (a → b) → b

ω m

# double mockingbird combinator
m' [[1 0 (1 0)]]

# owl combinator
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)]]]] ⧗ (b → c → d) → (a → b) → (a → c) → a → d

# psi combinator: on
ψ [[[[3 (2 1) (2 0)]]]] ⧗ (b → b → c) → (a → b) → a → a → c

ψ* [[[[[4 3 (2 1) (2 0)]]]]] ⧗ (c → b → b → d) → c → (a → b) → a → a → d

# queer bird combinator: reverse function composition: (f , g) x = g (f x)
q [[[1 (2 0)]]] ⧗ (a → b) → (b → c) → a → c

# quixotic bird combinator
q' [[[2 (0 1)]]] ⧗ (b → c) → a → (a → b) → c

# quizzical bird combinator
q'' [[[1 (0 2)]]] ⧗ a → (b → c) → (a → b) → c

# quirky bird combinator
q''' [[[0 (2 1)]]] ⧗ (a → b) → a → (b → c) → c

# quacky bird combinator
q'''' [[[0 (1 2)]]] ⧗ a → (a → b) → (b → c) → c

# robin combinator
r [[[1 0 2]]] ⧗ a → (b → a → c) → b → c

# robin once removed combinator
r* [[[[3 1 0 2]]]] ⧗ (b → c → a → d) → a → b → c → d

# robin twice removed combinator
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)]]] ⧗ (a → b → c) → (a → b) → a → c

…<*>… s

# thrush combinator: flipped $
t [[0 1]] ⧗ a → (a → b) → b

…&… t

# turing combinator
u [[0 (1 1 0)]]

# vireo combinator
v [[[0 2 1]]] ⧗ a → b → (a → b → c) → c

# vireo once removed combinator
v* [[[[3 0 2 1]]]] ⧗ (b → a → b → d) → a → b → b → d

# vireo twice removed combinator
v** [[[[[4 3 0 2 1]]]]] ⧗ (a → c → b → c → e) → a → b → c → c → e

# warbler combinator
w [[1 0 0]] ⧗ (a → a → b) → a → b

# warbler once removed combinator
w* [[[2 1 0 0]]] ⧗ (a → b → b → c) → a → b → c

# warbler twice removed combinator
w** [[[[3 2 1 0 0]]]] ⧗ (a → b → c → c → d) → a → b → c → d

# converse warbler combinator
w' [[0 1 1]] ⧗ a → (a → a → b) → b

# sage bird combinator
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]]] ⧗ (a → a) → a

# theta combinator
θ [[0 (1 1 0)]] [[0 (1 1 0)]]

# iota combinator
ι [0 s k]

# -- combinator equivalency tests --

:test (b) (s (k s) k)
:test (b') (b b b)
:test (b'') (b (b b b) b)
:test (b''') (b (b b) b)
:test (c) (s (b b s) (k k))
:test (c*) (b c)
:test (c**) (b c*)
:test (d) (b b)
:test (d') (b (b b))
:test (d'') (b b (b b))
:test (e) (b (b b b))
:test (e') (b (b b b) (b (b b b)))
:test (f) (e t t e t)
:test (f*) (b c* r*)
:test (f**) (b f*)
:test (g) (b b c)
:test (h) (b w (b c))
:test (i) (s k k)
:test (i*) (s (s k))
:test (j) (b (b c) (w (b c e)))
:test (ki) (k i)
:test (l) (c b m)
:test (m) (s i i)
:test (m') (b m)
:test (o) (s i)
:test (q) (c b)
:test (q') (b c b)
:test (q'') (c (b c b))
:test (q''') (b t)
:test (q'''') (f* b)
:test (r) (b b t)
:test (r*) (c* c*)
:test (r**) (b r*)
:test (t) (c i)
:test (u) (l o)
:test (v) (b c t)
:test (v*) (c* f*)
:test (v**) (b v*)
:test (w) (c (b m r))
:test (w*) (b w)
:test (w**) (b (b w))
:test (w') (c w)

# -- iota and SKI tests --

:test (i) (ι ι)
:test (k) (ι (ι (ι ι)))
:test (s) (ι (ι (ι (ι ι))))
:test (c) (s (s (k (s (k s) k)) s) (k k))
:test (w) (s s (s k))