Is there a relationship between visitor pattern and DeMorgan's Law?

Visitor Pattern enables mimicking sum types with product types. Where does the "sum"-iness come from?

For example, in OCaml one could define type my_bool = True | False

Or encode with visitor pattern:

type 'a bool_visitor = {
case_true: unit -> 'a;
case_false: unit -> 'a;
}

let t visitor = visitor.case_true ()
let f visitor = visitor.case_false ()

let visitor = {
case_true = (fun () -> "true");
case_false = (fun () -> "true");
}

let () = print_endline (t visitor) (* prints "true" *)


What's the best way of explaining the sum-type-to-visitor-pattern transformation? Is it:

• Of course + and * are interdefinable, what did I expect?
• Or is it that the left side of -> is the "negative" position and that this leads to a DeMorgan-law-like flip of sum and product?

I also wonder if this question is related to how one can use universally-quantified types to mimic existential types.

The best way to explain it is $$\mathsf{Bool} \to C \cong C \times C,$$ which is a special case of $$(A + B) \to C \cong (A \to C) \times (B \to C).$$ Read the above as follows: as sum is equivalent to a pair of visitors.
• I think you've given a nice restatement of the equivalence and I see how the equivalence is a consequence of the definitions if I read this as in Coq's Prop: gist.github.com/mheiber/872eddb8fdec21a8cb63b6a4d2710892. Maybe my original question didn't make sense. I was trying to get an intuition - is it helpful to think of the left side of -> as "negative" and that negativeness can flip things? A similar sort of thing seems to be happening with how existential types can be mimicked using nested universally-quanitifying functions. Commented Apr 17, 2021 at 20:08
• By the way, I think the example I gave is more similar to your second formula: $$(True + False) \to string \cong (True \to string) \times (False \to string).$$ Commented Apr 17, 2021 at 20:15
• One way to view types is "combinatorically" -- you count their (total) inhabitants -- in which case discriminated sum types correspond to numeric sums, and product types correspond to numeric products. In such a scheme, function types correspond to numerical exponents (a "product" for each element of the domain). Combinatorically, the question then becomes $$C^{A+B} \stackrel{?}{=} C^A \cdot C^B$$ Commented Apr 18, 2021 at 5:26
• @MaxHeiber: the law holds in any cartesian closed category, and in particular in a Heyting algebra (which corresponds to your loking at Prop). Regarding the difference between C and 1 \to C (which you write erroneously as $\mathrm{True} \to C$ and $\mathrm{False} \to C$ – wrong because $\mathrm{True}$ and $\mathrm{False}$ are not types but values), those two are again isomorphic. Commented Apr 18, 2021 at 8:54
• @CurtisF, that's exactly what I was looking for, the exponential notation helped. I should have remembered $$C^{A+B} = C^A \cdot C^B$$ from high school math: en.wikipedia.org/wiki/Exponentiation#Identities_and_properties Commented Apr 18, 2021 at 9:31