*Bounty: 100*

*Bounty: 100*

I have heard the simply typed lambda calculus is the internal language of Cartesian closed categories.

What’s the internal language of the opposite type of category?

The rules dual to currying and uncurrying are:

$$

mathrm{mal} : mathrm{Hom}(b, a + c) to mathrm{Hom}(b vdash a, c) \

mathrm{try} : mathrm{Hom}(b vdash a, c) to mathrm{Hom}(b, a + c) $$

I have the intuition the opposite category would correspond to continuation passing style or pattern matching but the opposite typing rules seem very strange and hard to figure out.

Trivially one could interpret/compile the simply typed lambda calculus in reverse but that would be extraordinarily confusing.

I have found with a little bit of finagling we can get rules that resemble continuation passing style.

$$

mathrm{kont} : mathrm{Hom}(x, b) to mathrm{Hom}(c, mathrm{0}) to mathrm{Hom}(x, b vdash c) \

mathrm{kont} , x , k = [mathrm{absurd} circ k , mathrm{id}] circ mathrm{try} , mathrm{id} circ x

$$

$$

mathrm{jump} : mathrm{Hom}(x, b vdash a) to mathrm{Hom}(b, a) to mathrm{Hom}(x, mathrm{0}) \ mathrm{jump} , k , x = mathrm{mal} , ( mathrm{i}_1 circ x ) circ k $$

$$ mathrm{env} : mathrm{Hom}(x, b vdash a) to mathrm{Hom}(x, b) \ mathrm{env} , k = mathrm{mal} , mathrm{i}_2 circ k$$

These are still pretty hard to figure out an interpretation for though.