Generic mappings over pairs

Browsing around on Oleg Kiselyov's excellent site, I came across a very interesting paper about "Advanced Polymorphism in Simpler-Typed Languages". One of the neat examples I'm about to present is concerned with expressing mappings over pairs that are generic not only in the datatypes involved but also over the number of arguments. The idea is to produce a family of functions $pair\_map_{i}$ such that

pair_map_1 f g (x, y) (x', y') → (f x, g y) 
pair_map_2 f g (x, y) (x', y') → (f x x', g y y') 
pair_map_3 f g (x, y) (x', y') (x'', y'', z'') → (f x x' x'', g y y' y'')
       .
       .
       .

The technique used to achieve this brings a whole bunch of functional programming ideas together : higher order functions, combinators and continuation passing style (and also leads into topics like the "value restriction" typing rules in the Hindley-Milner system).

let ( ** ) app k = fun x y -> k (app x y)
let pc k a b = k (a, b)
let papp (f1, f2) (x1, x2) = (f1 x1, f2 x2)
let pu x = x

With the above definitions, $pair\_map_{i}$ is generated like so.

(*The argument [f] in the below is for the sake of value restriction*)
let pair_map_1 f = pc (papp ** pu) (f : α -> β)
let pair_map_2 f = pc (papp ** papp ** pu) (f : α -> β -> γ)
let pair_map_3 f = pc (papp ** papp ** papp ** pu) (f : α -> β -> γ -> δ)

For example,

# pair_map_2 ( + ) ( - ) (1, 2) (3, 4) ;;
- : int * int = (4, -2)

Reverse engineering how this works requires a bit of algebra.

Let's tackle $pair\_map_{1}$. First

pc (papp ** pu) = (λk f g. k (f, g)) (papp ** pu) = λf g. (papp ** pu) (f, g)

and,

papp ** pu = λx y. pu (papp x y) = λx y. papp x y

so,

λf g. (papp ** pu) (f, g) =
    λf g. (λ(a, b) (x, y). (a x, b y)) (f, g) =
    λf g (x, y). (f x, g y)

that is, pair_map_1 = pc (papp ** pu) = λf g (x, y). (f x, g y) and, we can read the type off from that last equation as (α → β) → (γ → δ) → α * γ → β * δ.

Now for $pair\_map_{2}$. We have

pc (papp ** papp ** pu) =
    (λk f g. k (f, g)) (papp ** papp ** pu) =
    λf g. (papp ** papp ** pu) (f, g)

where,

papp ** papp ** pu = papp ** (papp ** pu) =
    papp ** (λa' b'. pu (papp a' b')) =
    papp ** (λa' b'. papp a' b') = 
    λa b. (λa' b'. papp a' b') (papp a b)

which means,

pc (papp ** papp ** pu) = 
    λf g. (papp ** papp ** pu) (f, g) =
    λf g. (λa b.(λa' b'. papp a' b') (papp a b)) (f, g) =
    λf g. (λb. (λa' b'. papp a' b') (papp (f, g) b)) =
    λf g. λ(x, y). λa' b'. (papp a' b') (papp (f, g) (x, y)) =
    λf g. λ(x, y). λa' b'. (papp a' b') (f x, g y) =
    λf g. λ(x, y). λb'. papp (f x, g y) b' =
    λf g. λ(x, y). λ(x', y'). papp (f x, g y) (x', y') =
    λf g (x, y) (x', y'). (f x x', g y y')

that is, a function in two binary functions and two pairs as we expect. Phew! The type in this instance is (α → β → γ) → (δ → ε → ζ) → α * δ → β * ε → γ * ζ.

To finish off, here's the program transliterated into C++(14).

#include <utility>
#include <iostream>

//let pu x = x
auto pu = [](auto x) { return x; };

//let ( ** ) app k  = fun x y -> k (app x y)
template <class F, class K>
auto operator ^ (F app, K k) {
  return [=](auto x) {
    return [=] (auto y) {
      return k ((app (x)) (y));
    };
  };
}

//let pc k a b = k (a, b)
auto pc = [](auto k) {
  return [=](auto a) {
    return [=](auto b) { 
      return k (std::make_pair (a, b)); };
  };
};

//let papp (f, g) (x, y) = (f x, g y)
auto papp = [](auto f) { 
  return [=](auto x) { 
    return std::make_pair (f.first (x.first), f.second (x.second)); };
};

int main () {

  auto pair = &std::make_pair<int, int>;

  {
  auto succ= [](int x){ return x + 1; };
  auto pred= [](int x){ return x - 1; };
  auto p  = (pc (papp ^ pu)) (succ) (pred) (pair (1, 2));
  std::cout << p.first << ", " << p.second << std::endl;
  }

  {
  auto add = [](int x) { return [=](int y) { return x + y; }; };
  auto sub = [](int x) { return [=](int y) { return x - y; }; };
  auto p = pc (papp ^ papp ^ pu) (add) (sub) (pair(1, 2)) (pair (3, 4));
  std::cout << p.first << ", " << p.second << std::endl;
  }

  return 0;
}