Primitive functions for functions [dt-002P]
DefinitionThe \mathit {apply} function [dt-002N]
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]
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.
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.
- \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.
DefinitionThe \mathit {curry} function [dt-002O]
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}
TheoremContinuity of \mathit {curry} [dt-002S]
- \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]
What is the common (functional programming) name for \mathit {apply} \circ (f \times \mathsf {id})?
\mathit {uncurry}Solution.