HiveBrain v1.2.0
Get Started
← Back to all entries
patternMinor

What is the name of this type of function composition?

Submitted by: @import:stackexchange-cs··
0
Viewed 0 times
thisthewhatfunctiontypenamecomposition

Problem

If standard function composition is defined as:

(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)$.

Context

StackExchange Computer Science Q#72603, answer score: 2

Revisions (0)

No revisions yet.