Exercise. [dt-002R]

Liam O'Connor

What is the common (functional programming) name for $\mathit {apply} \circ (f \times \mathsf {id})$ ?

Solution.

Liam O'Connor

$\mathit {uncurry}$

Context

Primitive functions for functions [dt-002P]

Liam O'Connor

Definition. The $\mathit {apply}$ function [dt-002N]

Liam O'Connor

The $\mathit {apply}$ function simply applies a given function to a given argument: $\begin {array}{l} \mathit {apply} : ((A \twoheadrightarrow B) \times A) \twoheadrightarrow B\\ \mathit {apply} (f, a) = f(a) \end {array}$

Exercise. [dt-002Q]

Liam O'Connor

Show that $\mathit {apply}$ is continuous.

Hint: A function $f : A \times B \rightarrow C$ is continuous iff it is continuous in each argument separately, i.e., iff $\forall a \in A.\ f(a,\cdot ) : B \rightarrow C$ is continuous, and $\forall b \in B.\ f(\cdot ,b) : A \rightarrow C$ is continuous.

Solution.

Liam O'Connor

First showing $\mathit {apply}(f,\cdot )$ is continuous for some continuous $f : A \twoheadrightarrow B$ , using the alternative characterisation

$\mathit {apply}(f,\cdot )$ is monotonic: Given $a, b \in A$ where $a \sqsubseteq b$ , we can see that $\mathit {apply}(f,a) = f(a) \sqsubseteq f(b) = \mathit {apply}(f,b)$ by the monotonicity of $f$ .
$\mathit {apply}(f,\cdot )$ preserves lubs: Given a directed $X \subseteq A$ , we can see that $\mathit {apply}(f,\bigsqcup X) = f(\bigsqcup X) = \bigsqcup \{f(x) \mid x \in X\} = \bigsqcup \{\mathit {apply}(f,x) \mid x \in X\}$ follows from the continuity of $f$ .

Next, showing

\mathit {apply}(\cdot ,a)

is continuous for some fixed

a \in A

:

$\mathit {apply}(\cdot ,a)$ is monotonic: Given $f, g \in A \twoheadrightarrow B$ where $f \sqsubseteq g$ , we can see that $\mathit {apply}(f,a) = f(a) \sqsubseteq g(a) = \mathit {apply}(g,a)$ by the pointwise ordering of functions.
$\mathit {apply}(\cdot ,a)$ preserves lubs: Given a directed $X \subseteq A \twoheadrightarrow B$ , we can see that $\mathit {apply}(\bigsqcup X, a) = \left (\bigsqcup X\right )(a) = \bigsqcup \{f(a) \mid f \in X\} = \bigsqcup \{\mathit {apply}(f,a) \mid f \in X\}$ follows from the lub definition for functions.

Definition. The $\mathit {curry}$ function [dt-002O]

Liam O'Connor

The function $\mathit {curry}$ transforms a function that takes two arguments all at once (as a product) into a function that takes the arguments one at a time. That is, if $f : A \times B \twoheadrightarrow C$ then: $\begin {array}{l} \mathit {curry}(f) : A \twoheadrightarrow (B \twoheadrightarrow C)\\ \mathit {curry}(f)(a)(b) = f(a, b) \end {array}$

Theorem. Continuity of $\mathit {curry}$ [dt-002S]

Liam O'Connor

$\mathit {curry}$ is continuous on $A \times B \twoheadrightarrow C$ .
$\mathit {curry}(f)$ , given continuous $f : A \times B \twoheadrightarrow C$ , is continuous on $A$ .
$\mathit {curry}(f)(a)$ , given continuous $f : A \times B \twoheadrightarrow C$ and $a \in A$ , is continuous on $B$ .

Exercise. [dt-002R]

Liam O'Connor

What is the common (functional programming) name for $\mathit {apply} \circ (f \times \mathsf {id})$ ?

Solution.

Liam O'Connor

$\mathit {uncurry}$

Backlinks

Theorem. The currying isomorphism [dt-002U]

Liam O'Connor

(A \times B)\twoheadrightarrow C \;\;\simeq \;\; A\twoheadrightarrow (B\twoheadrightarrow C)

Proof.

Liam O'Connor

Follows from the universal property for functions when set up with the isomorphism from curry and its inverse, the function in Exercise [dt-002R].