patternMinor
What is the name of this type of function composition?
Viewed 0 times
thisthewhatfunctiontypenamecomposition
Problem
If standard function composition is defined as:
What type of composition does the below function describe? Is there a particular name for it in category theory?
(define compose
{ (B → C) → (A → B)
→ (A → C) }
F G -> (λ X (F (G X))))What type of composition does the below function describe? Is there a particular name for it in category theory?
(define compose-2
{ (A → (X → C)) → (B → X)
→ (A → B → C) }
F G -> (λ Y (compose (F Y) G)))Solution
You composition is of type $\operatorname{comp}:(A \to X \to C)\to (B \to X) \to (A\to B \to C)$. Up to Currying, it can be seen as being of type $(A \times X \to C)\to (B \to X) \to (A\times B \to C)$. So it's just a composition of a two arguments functions with a one argument function. You take $f$ and $g$ and return $(a,b)\mapsto f(a,g(b))$.
From a general abstract nonsense point of view, you can define the functor $$A\times -:\begin{array}{lll}
O & \mapsto &A\times O\\
g : B \to X&\mapsto &:A\times B \to A\times X
\end{array}$$
and then your composition is just $\operatorname{comp}=f\mapsto g \mapsto f\circ (A\times g)$.
From a general abstract nonsense point of view, you can define the functor $$A\times -:\begin{array}{lll}
O & \mapsto &A\times O\\
g : B \to X&\mapsto &:A\times B \to A\times X
\end{array}$$
and then your composition is just $\operatorname{comp}=f\mapsto g \mapsto f\circ (A\times g)$.
Context
StackExchange Computer Science Q#72603, answer score: 2
Revisions (0)
No revisions yet.