Why does my pattern block an error on both sides?

Question

To start off this whole thing I'm working with a pattern synonym defined as follows:

{-# Language PatternSynonyms #-}

pattern x := y <- x @ y

This allows me to run multiple pattern matches across a parameter at once. A regular as binding (@) does not allow the left hand side to be a pattern but this does.

With this I make the following toy function

{-# Language ViewPatterns #-}
f ((_:_) := (head -> y)) =
  [ y ]
f [] =
  []

It's not the best way to implement this I am sure, but it's a minimum working example for the behavior in question.

This has a function that takes a single parameter. It matches the parameter against two patterns using the defined synonym. The first pattern matches any non-empty list and makes no bindings. The second runs the head function on the list and binds y to the result.

So the question is can head cause an error or will the other pattern prevent it?

>>> f []
[]

The other pattern prevents it! Alright so if I do them in the other order then it should break right?

f' ((head -> y) := (_:_)) =
  [ y ]
f' [] =
  []

>>> f' []
[]

Nope! It still works. So now my question is: Is the second pattern doing anything at all? Maybe view patterns has some sort of smart behavior where it calls the function and fails the pattern if an error occurs ...

f'' (head -> y) =
  [ y ]
f'' [] =
  []

>>> f'' []
[*** Exception: Prelude.head: empty list

No ... it doesn't. This fails. Somehow (_:_) blocks the error no matter what side it's on. Maybe ghc prefers to match destructuring patterns before view patterns? To test this I can replace the pattern (_:_) with (reverse -> _:_). This way it has to run a function before it can get to the destructuring.

But having tested it, the new pattern doesn't change the behavior. This hypothesis can be ruled out.

So maybe it's laziness? x can't be evaluated if the list is empty so it sits in thunk and the error never occurs. It seems to somewhat be the case. If I replace (head -> x) with (undefined -> x) we have no change in behavior.

However if I replace it with (undefined -> "yo"):

f ((undefined -> "yo") := (x:_)) = [x]
f [] = []

>>> f []
*** Exception: Prelude.undefined

The undefined does get evaluated. Which seems to indicate that the pattern is forcing evaluation to compare with "yo". And if I now switch the order:

f ((x:_) := (undefined -> "yo")) = [x]
f [] = []

>>> f []
[]

It isn't evaluated. It seems that now we are short circuiting the pattern match.

So the laziness hypothesis seems to make sense? It's still very opaque to me and I would love to have someone with more experience as to the internals of ghc confirm this hypothesis.

So my question is now what is going on? Is it laziness? How does it work?

A big thanks to discord user lexi. They helped a lot in the diagnosis thus far.

Answer 1

You are indeed observing the effect of laziness.

Let's start with a much more basic example:

f :: () -> Int
f x = 42

Laziness makes f undefined return 42. This is because the variable pattern x does not require the argument to be evaluated, so undefined is never demanded.

By comparison, if we used

f :: () -> Int
f () = 42

then f undefined does crash, since the pattern () requires the argument to be evaluated until it exposes the () constructor (which, in this case, means fully evaluated).

Similarly,

f :: String -> Int
f x = 42

will cause f undefined to return 42, while

f :: String -> Int
f (x:xs) = 42

will cause f undefined to crash, after trying to evaluate undefined so to expose the first list constructor (either : or []).

We also have that

f :: String -> Int
f "yo" = 42
f x    = 0

makes f undefined crash: after all the pattern "yo" means ('y':'o':[]) so it will force undefined, trying to match it against the first :. More in detail, all the following calls will crash:

f undefined
f (undefined:anything)
f ('y':undefined)
f ('y':undefined:anything)
f ('y':'o':undefined)

Here anything can be undefined or any other string/char as needed.

By comparison, all of the following calls will return 0 since the first pattern in the definition fails its match (without crashing!):

f []
f ('a':anything)
f ('y':'a':anything)
f ('y':'o':anything:anything)

Again, anything can be undefined or any other string/char as needed.

This is because the pattern matching of "yo" is done roughly like this:

• evaluate the input value x until WHNF (expose its first constructor)
  • if it is [], fail
  • if it is y:ys, evaluate y until WHNF
    • if y is another char than 'y', fail
    • if y is 'y', evaluate ys until WHNF
      • if it is '[]`, fail
      • if it is z:zs, evaluate z until WHNF
        • if z is another char than 'o', fail
        • if z is 'o', evaluate zs until WHNF
          • if it is [], succeed!!
          • if it is h:hs, fail

Note that in each "evaluate .. until WHNF" point we could crash (or get stuck in an infinite computation) beacuse of bottoms.

Essentially, pattern matching proceed left-to-right and stops, evaluating the input only as much as needed, and stopping as soon as the result (fail/success) is known. This will not necessarily force the full evaluation of the input. On failure, we do not even necessarily evaluate the input as deep as the pattern, if we discover an early failure point. This is indeed what happens when you write:

It seems that now we are short circuiting the pattern match.

Now, view patterns follow the same principle. A pattern undefined -> x will not evaluate undefined on the input since x does not need to know the result of undefined to succeed. Instead undefined -> x:xs, undefined -> [], and undefined -> "yo" do need to know the result, hence they will evaluate it as needed.

About your examples:

f ((_:_) := (head -> y))

Here, head -> y always succeeds. On its own, it could bind y to a bottom value, but that's prevented by the leftmost _:_ pattern.

f' ((head -> y) := (_:_))

Here, head -> y always succeeds. On its own, it will bind y to a bottom value, and this actually happens if the input is [], but that will not force the input, so not crash is caused so far. After that, we try the leftmost _:_ pattern, which fails. Result: failure, but no crash.

f'' (head -> y) = [ y ]

Again, head -> y always succeeds, and binds y to bottom (if the input is []). The pattern matching will succeed, and the result of f'' is [ head [] ]. We can take, e.g., the length of this list, but we can not print its contents without crashing.

f ((undefined -> "yo") := (x:_)) = [x]
f [] = []

undefined -> "yo" crashes, as explained above. The x:_ pattern is never tried.

f ((x:_) := (undefined -> "yo")) = [x]

Here we first match x:_ and only when that succeeds we try undefined -> "yo". Since we call f with [], the view pattern is not tried, so it does not crash. Calling f "a" would instead match x:_, try the view pattern and crash.