Comment by nimih

Comment by nimih 3 days ago

0 replies

Somewhat surprisingly (to me at least), this puzzle is "solvable" pretty quickly by using the Haskell typechecker interactively. Here's what I did, along with the compiler's error messages.

Start with some definitions:

    c :: (b -> c) -> (a -> b) -> (a -> c)
    c = \g f x -> g (f x) -- alternatively, c = (.)

    answer :: (y -> z) -> (x -> y) -> (w -> x) -> (w -> z)
    answer = undefined
We need to start somewhere:

    answer = c

    - Couldn't match type ‘x’ with ‘w -> x’
      Expected: (y -> z) -> (x -> y) -> (w -> x) -> w -> z
        Actual: (y -> z) -> (x -> y) -> x -> z
Okay, we knew this wouldn't work, does a solution exist if we apply `c` to a single argument?

    answer = c _1
    
    - Couldn't match type ‘y’ with ‘x -> y’
      Expected: (y -> z) -> (x -> y) -> (w -> x) -> w -> z
        Actual: (y -> z) -> y -> (w -> x) -> w -> z

    - Found hole: _1 :: z -> (w -> x) -> w -> z
Nope, it can't: `c` allows its 3rd argument to be an arbitrary type `y`, but we know the corresponding argument to `answer` should be constrained to a function type `x -> y`. So we need to fully apply `c`.

    answer = c _1 _2

    - Found hole: _1 :: b0 -> (x -> y) -> (w -> x) -> w -> z
      Where: ‘b0’ is an ambiguous type variable

    - Found hole: _2 :: (y -> z) -> b0
      Where: ‘b0’ is an ambiguous type variable
Okay, great, we'll be done if we can find values for our typed holes. Again, we need to start somewhere:

    answer = c c _2

    - Couldn't match type ‘x’ with ‘w -> x’
      Expected: (y -> w -> z) -> (x -> y) -> (w -> x) -> w -> z
        Actual: (y -> w -> z) -> (x -> y) -> x -> w -> z

    - Found hole: _2 :: (y -> z) -> y -> w -> z
Again, the shape of [the 2nd] `c` is wrong here: we need a function whose 3rd argument is a function of some sort, not an arbitrary type (NB in retrospect we could've realized this by looking at the shape of `_1`'s type). Let's try the simplest possible option:

    answer = c (c _3) _2

    - Found hole: _3 :: b0 -> (w -> x) -> w -> z
      Where: ‘b0’ is an ambiguous type variable

    - Found hole: _2 :: (y -> z) -> (x -> y) -> b0
      Where: ‘b0’ is an ambiguous type variable
We seem to be on the right track here: the 2nd `c` now typechecks. Even better, `_3` has a familiar looking type: it looks suspiciously similar to the type of `c`. Let's see if that works.

    answer = c (c c) _2

    - Found hole: _2 :: (y -> z) -> (x -> y) -> x -> z
      Where: ‘y’, ‘x’, ‘z’ are rigid type variables bound by
The final piece of the puzzle is now hopefully obvious:

    answer = c (c c) c
Much like the article's author (which I read after finding my own solution), I don't feel like I gained any great insight through this process, other than how useful it is to have good compiler error messages alongside features like typed holes.