1
$\begingroup$

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.

$\endgroup$
1
2
$\begingroup$

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.

(By the way, this is not the de Morgan law. It does not have a name, as far as I know. It's a general consequence of the definition of the concepts involved.)

$\endgroup$
5
  • $\begingroup$ 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. $\endgroup$ – Max Heiber Apr 17 at 20:08
  • $\begingroup$ 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).$$ $\endgroup$ – Max Heiber Apr 17 at 20:15
  • 1
    $\begingroup$ 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 $$ $\endgroup$ – Curtis F Apr 18 at 5:26
  • 1
    $\begingroup$ @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. $\endgroup$ – Andrej Bauer Apr 18 at 8:54
  • $\begingroup$ @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 $\endgroup$ – Max Heiber Apr 18 at 9:31

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.