sgreben

Purely mechanically. Just writing down the problem statement we get:

    \exists f,g: \forall a,b: (f(b)=a) | (g(a)=b)

where f,g are the guesses and a,b are the flips. Each guess is a function of the information available to the respective player -- the outcome of his own coin flip. There's only 4 unary boolean functions:

    f,g \in {true,false,id,not} 

The constant functions are out and order doesn't matter, so we're left with

    {(id,not),(id,id),(not,not)}

Here I just tried (id,not) first, but 3 choices are easy to check exhaustively.

I'm not proposing this as a solution to the expression problem (which has actual solutions, as noted in the other comments [0] and elsewhere [1]).

It is, however, an extremely simple way of implementing the table-style dispatch outlined in the post, with a reasonable layout and compile-time completeness checks.

It's not open to extension outside the compilation unit, but in exchange it is dead simple and you still only ever need to change exactly two places in the code if you want to extend along either axis. Sometimes you just don't need polymorphism when a switch statement will do.

[0] https://news.ycombinator.com/item?id=9409779 [1] (PDF) http://www.math.nagoya-u.ac.jp/~garrigue/papers/variant-reus...

Sum types + exhaustiveness checking already do this, right? For this example:

  type animal = Cat | Dog
  type action = Sound | Eat | Attack

  let cat_sound () = printf "meow"
  let cat_attack () = printf "scratch"
  let dog_sound () = printf "woof"

  let act animal action = match animal,action with
  | Cat, Sound  -> cat_sound ()
  | Cat, Attack -> cat_attack ()
  | Dog, Sound  -> dog_sound ()

Compiling this yields:

  Warning 8: this pattern-matching is not exhaustive.
  Here is an example of a value that is not matched:
  (Dog, (Eat|Attack))

just as we'd like.