Right Associativity
Identity Function aka id
id a ≝ a
id ≝ λ a . a abstraction
Application Function aka apply or $
apply f a ≝ f a reification
apply f ≝ λ a . f a abstraction
apply f ≝ f η-reduction
apply ≝ λ f . f abstraction
apply ≝ id rewrite
High Order Function
"Transformation" Function
Composition Function aka ∘
Pipelining Function aka |>
Abstraction over Type Constructors
Function Mapping aka fmap
Lifting Function aka pure
Applicative Functor aka <∗>
Given
fmap f ≝ ?
(a → b) → ?
fmap f ≝ f
(a → b) → (a → b)
fmap f ≝ pure f
(a → b) → m (a → b)
fmap f ≝ pure f <∗>
(a → b) → (m a → m b)
Flattening Function aka join
Combining Computation Function aka bind
Given
bind f ≝ ?
(a → m b) → ?
bind f ≝ f
(a → m b) → (a → m b)
bind f ≝ fmap f
(a → m b) → (m a → m (m b))
bind f ≝ fmap f |>
(a → m b) → (m (m b) → ?) → (m a → ?)
bind f ≝ fmap f |> join
(a → m b) → (m a → m b)
Kleisli Monad Pipelining aka >=>
Given
f >=> g ≝ ?
(a → m b) → (b→ m c) → ?
f >=> g ≝ f
(a → m b) → (b→ m c) → (a → m b)
f >=> g ≝ f |>
(a → m b) → (b→ m c) → (m b → ?) → (a → ?)
f >=> g ≝ f |>
g :: b → m c
(a → m b) → (b→ m c) → (m b → ?) → (a → ?)
f >=> g ≝ f |>
bind g :: m b → m c
(a → m b) → (b→ m c) → (m b → ?) → (a → ?)
f >=> g ≝ f |> (bind g)
(a → m b) → (b→ m c) → (a → m c)
(a → m b) → (m a → m b) | Function centric |
m a → (a → m b) → m b | Data centric |
Function centric approach promotes the composition
(bind f) >=> g ≡ (bind f) |> (bind g) -- rewrite ≡ (bind g) . (bind f) -- rewrite ≡ a → (bind g) . (bind f) a -- η-expansion ≡ a → bind g (bind f a) -- rewrite ≡ a → bind (x → (bind g) (f x)) a -- bind associativity ≡ a → bind (x → (bind g) . f x) a -- rewrite ≡ a → bind ((bind g) . f) a -- η-reduction ≡ a → bind (f |> (bind g)) a -- rewrite ≡ bind (f |> (bind g)) -- η-reduction ≡ bind (f >=> g) -- rewrite
(f >=> g) >=> r ≡ (f |> (bind g)) |> (bind r) -- rewrite ≡ f |> ((bind g) |> (bind r)) -- Pipelining associativity ≡ f |> ((bind g) >=> r) -- rewrite ≡ f |> (bind (g >=> r)) -- Bind-Kleisli rewrite ≡ f >=> (g >=> r) -- rewrite